Zusammenfassung
In der Praxis sind nicht nur die Erfüllbarkeit von Formeln und die Algorithmen zu ihrer Entscheidung wichtig. Häufig steht auch die Frage im Vordergrund, ob aus einer logischen Beschreibung ein bestimmter Sachverhalt, d.h. eine weitere Formel gefolgert werden kann. Natürlich ist die semantische Folgerbarkeit mit dem Umweg über die Erfüllbarkeit beantwortbar, indem wir das Deduktionstheorem für ⊨ ausnutzen, d.h. die Äquivalenz „α ⊨ β ⇔ (α Λ ¬β) nicht erfüllbar“.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1994 B. G. Teubner Stuttgart
About this chapter
Cite this chapter
Büning, H.K., Lettmann, T. (1994). Resolution. In: Aussagenlogik: Deduktion und Algorithmen. Leitfäden und Monographien der Informatik. Vieweg+Teubner Verlag. https://doi.org/10.1007/978-3-322-84809-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-322-84809-3_4
Publisher Name: Vieweg+Teubner Verlag
Print ISBN: 978-3-519-02133-9
Online ISBN: 978-3-322-84809-3
eBook Packages: Springer Book Archive