Buch, Deutsch, 438 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 680 g
Deduktion und Algorithmen
Buch, Deutsch, 438 Seiten, Format (B × H): 155 mm x 235 mm, Gewicht: 680 g
Reihe: Leitfäden und Monographien der Informatik
ISBN: 978-3-519-02133-9
Verlag: Vieweg+Teubner Verlag
Die Ausgangsbasis fiir die Erstellung dieses Buches waren Vorlesungen iiber Grundlagen wissensbasierter Systeme und iiber Deduktionssysteme. Ein zen trales Thema dieser Veranstaltungen ist die Frage, inwieweit und mit wel chen Verfahren man entscheiden kann, ob aus einem Ausdruck ein anderer Ausdruck folgt. Flir die Pradikatenlogik und deren Teilklassen tritt diese Problemstellung z.B. in der Logik-Programmierung, dem automatischen Be weisen, in Inferenzkomponenten wissensbasierter Systeme und - aquivalent formuliert - als Erfiillbarkeitsproblem auf. Es hat sich dabei herausgestellt, daB selbst die fiir die Aussagenlogik interes santen Resultate zu reichhaltig sind, urn sie zusammen mit der Pradikaten logik in nur einem Zyklus zu behandeln. Da aber viele Ergebnisse fiir eine effiziente Behandlung der vollen Pradikatenlogik von groBem N utzen sind, haben wir uns entschlossen, die Themenbereiche, die von allgemeinem Inter esse sind, zu sammeln, zusammenhangend aufzuarbeiten und in Buchform zu veroffentlichen. Aber selbst die Beschrankung auf die Aussagenlogik ist nicht ausreichend, urn wirklich aile Problemstellungen und Ansatze aufzu nehmen. Wir haben daher hier zu Gunsten der Grundlagen und von eher klassischen Inhalten auf Abschnitte iiber z.B. die mehrwertige Aussagenlogik verzichtet.
Zielgruppe
Professional/practitioner
Weitere Infos & Material
1 Einführung in die Aussagenlogik.- 1.1 Syntax und Semantik der Aussagenlogik.- 1.2 Einfache Zusammenhänge.- 1.3 Übungsaufgaben.- 2 Datenstrukturen und Normalformen.- 2.1 Allgemeine Datenstruktur für aussagenlogische Formeln.- 2.2 Negationsnormalform (NNF).- 2.3 Konjunktive Normalform.- 2.4 Weitere Normalformen.- 2.5 Übungsaufgaben.- 3 Erfüllbarkeit.- 3.1 Komplexität von Erfüllbarkeitsproblemen.- 3.2 Sammlung von aussagenlogischen Problemen.- 3.3 Erfüllbarkeit und 2-KNF.- 3.4 Davis-Putnam-Algorithmen.- 3.5 Komplexitätsanalyse von Davis-Putnam-Algorithmen.- 3.6 Relaxations-Algorithmus.- 3.7 Unabhängige Klauseln.- 3.8 Konnektionsmethode.- 3.9 Partielle Erfüllbarkeitsalgorithmen.- 3.10 Verteilung erfüllbarer Formeln.- 3.11 Übungsaufgaben.- 4 Resolution.- 4.1 Grundlagen der Resolution.- 4.2 Länge von Resolutionsbeweisen.- 4.3 Resolutionsstrategien.- 4.4 Klauselorientierte Resolution.- 4.5 Übungsaufgaben.- 5 Horn-Logik.- 5.1 Grundlagen.- 5.2 Umbenennung.- 5.3 Unit-Resolution.- 5.4 Unique-Satisfiability für Horn-Formeln.- 5.5 Reduktion von Horn-Formeln.- 5.6 Äquivalenzprobleme.- 5.7 SLD-Resolution.- 5.8 Erweiterung der Horn-Logik.- 5.9 Übungsaufgaben.- 6 Kalküle.- 6.1 Frege-Systeme.- 6.2 Lineare Ungleichungssysteme.- 6.3 Tableau-Kalküle.- 6.4 Der Sequenzenkalkül.- 6.5 Vergleich aussagenlogischer Beweissysteme.- 7 Quantifizierte Formeln.- 7.1 Einführung.- 7.2 Normalformen.- 7.3 Q-Resolution.- 7.4 Q-Unit-Resolution.- 7.5 Quantifizierte HORN-Formeln.- 7.6 Quantifizierte 2-KNF-Formeln.- 7.7 Übungsaufgaben.- Algorithmenverzeichnis.- Symbolverzeichnis.
