Zusammenfassung
In den bisherigen Kapiteln haben wir verschiedene Algorithmen für den Test auf Erfüllbarkeit von Formeln vorgestellt und analysiert. Desweiteren haben wir die Resolution als mächtigen Kalkül für die Verarbeitung von Formeln in Konjunktiver Normalform, speziell für Horn—Formeln kennengelernt. Allerdings ist dieser Kalkül nur widerlegungsvollständig. Es läßt sich mit Hilfe der Herleitungsregeln nur feststellen, ob eine Formel widerspruchsvoll ist.
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). Kalküle. In: Aussagenlogik: Deduktion und Algorithmen. Leitfäden und Monographien der Informatik. Vieweg+Teubner Verlag. https://doi.org/10.1007/978-3-322-84809-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-322-84809-3_6
Publisher Name: Vieweg+Teubner Verlag
Print ISBN: 978-3-519-02133-9
Online ISBN: 978-3-322-84809-3
eBook Packages: Springer Book Archive