Zusammenfassung
Jetzt übertragen wir einige wichtige Ergebnisse des 2. Teils — Semi-Entscheidungsverfahren und Endlichkeitssätze, nicht dagegen Vollständigkeit — auf die Quantorenlogik und gewinnen so wichtige, aber auch überraschende Ergbenisse. Als erstes stellen wir die Theorembeweiser, von denen Clarissa in der Einleitung zu Teil 2 gesprochen hat, für die Prädikatenlogik auf. Dazu setzen wir alles zusammen, was wir bisher gelernt haben: Mit Hilfe der Ergebnisse aus 3A überführen wir Formeln in pränexe Normalform (3B1) und beseitigen dann die Quantoren durch Skolemisieren (3B2). Die entstehenden quantorenfreien Formeln können wir in die Theorembeweiser aus 2D5 oder 2D6 eingeben (3B3). Als Anwendung benutzen wir Theorembeweiser, um Beispielterme für Existenzformeln zu finden (3B4). Damit formulieren wir das alte Ergebnis von Herbrand um, das wir in Abschnitt 2D6 in einer Fassung fürs Theorembeweisen gebracht haben, und verallgemeinern es fürs logische Programmieren. In 3B5 spezialisieren wir das Verfahren für Hornformeln und erläutern so die Vorgehensweise, die PROLOG zugrundeliegt. In 3B6 zeigen wir, daß auch in der Prädikatenlogik jede erfüllbare Formelmenge ein Herbrandmodell hat und folgern daraus in 3B7, daß es zu jeder Struktur eine äquivalente (die selben Formeln erfüllende) höchstens abzählbare gibt (Satz von Löwenheim und Skolem). In 3B8 schließlich gewinnen wir aus dem Vollständigkeitsden Kompaktheits- und den Endlichkeitssatz wieder Als erste Konsequenz daraus bedrohen uns Monster in Architektenstrukturen, die uns in Kap. 3C in den natürlichen Zahlen heilsame Lehren erteilen werden.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Rights and permissions
Copyright information
© 1990 Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig
About this chapter
Cite this chapter
Siefkes, D. (1990). Finitisieren und mechanisieren. In: Formalisieren und Beweisen. Lehrbuch. Vieweg+Teubner Verlag, Wiesbaden. https://doi.org/10.1007/978-3-322-85621-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-322-85621-0_11
Publisher Name: Vieweg+Teubner Verlag, Wiesbaden
Print ISBN: 978-3-528-04757-3
Online ISBN: 978-3-322-85621-0
eBook Packages: Springer Book Archive