Aussagenlogik Deduktion und Algorithmen Deduktion und Algorithmen [Paperback]

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.3.1 Datenstruktur f?r Konjunktive Normalform.- 2.4 Weitere Normalformen.- 2.4.1 Disjunktive Normalform.- 2.4.2 Binary Decision Diagrams.- 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.3.1 Stufens?ttigungsstrategie.- 4.3.2 St?tzmengenrestriktion und semantische Resolution.- 4.3.3 P- und N-Resolution.- 4.3.4 Hyperresolution.- 4.3.5 Lineare Resolution.- 4.3.6 Resolution mit geordneten Klauseln.- 4.3.7 Lock-Resolution.- 4.3.8 Regul?re Resolution.- 4.3.9 Davis-Putnam-Resolution.- 4.3.10 Input-Resolution.- 4.3.11 Unit-Resolution.- 4.3.12 Unit-Preference-Strategie.- 4.3.13 Platzbeschr?nkte Resolution.- 4.3.14 Extended Resolution.- 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.7.1 Ein Linearzeit-Algorithmus f?r die Prolog-Funktion.- 5.7.2 Schleifen und ?quivalenz bei Prolog.- 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.4.1 Der Sequenzenkalk?l von Gentzen.- 6.4.2 Ein modiflc»