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.
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.
Inhaltsverzeichnis
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.
