reine Buchbestellungen ab 5 Euro senden wir Ihnen Portofrei zuDiesen Artikel senden wir Ihnen ohne weiteren Aufpreis als PAKET

Aussagenlogik: Deduktion und Algorithmen
Deduktion und Algorithmen
Theodor Lettmann

Print on Demand - Dieser Artikel wird für Sie gedruckt!

59,99 €

inkl. MwSt. · Portofrei
Dieses Produkt wird für Sie gedruckt, Lieferzeit ca. 14 Werktage
Menge:

Produktbeschreibung

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 modifizierter Sequenzenkalkül.- 6.4.3 Herleitung von Tableau-Kalkiilen.- 6.5 Vergleich aussagenlogischer Beweissysteme.- 6.5.1 Übungsaufgaben.- 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.5.1 Erfüllbarkeitsproblem für QHORN.- 7.5.2 Folgerung und Äquivalenz.- 7.6 Quantifizierte 2-KNF-Formeln.- 7.7 Übungsaufgaben.- Algorithmenverzeichnis.- Symbolverzeichnis.
"... Dieses Lehrbuch ... stellt die Grundlagen dieses Gebiets ausführlich und umfassend ... dar." P. Schmitt. Internationale Mathematische Nachrichten, Wien
"... Dieses Lehrbuch ... stellt die Grundlagen dieses Gebiets ausführlich und umfassend ... dar." P. Schmitt. Internationale Mathematische Nachrichten, Wien
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 modifizierter Sequenzenkalkül.- 6.4.3 Herleitung von Tableau-Kalkiilen.- 6.5 Vergleich aussagenlogischer Beweissysteme.- 6.5.1 Übungsaufgaben.- 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.5.1 Erfüllbarkeitsproblem für QHORN.- 7.5.2 Folgerung und Äquivalenz.- 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.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 modifizierter Sequenzenkalkül.- 6.4.3 Herleitung von Tableau-Kalkiilen.- 6.5 Vergleich aussagenlogischer Beweissysteme.- 6.5.1 Übungsaufgaben.- 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.5.1 Erfüllbarkeitsproblem für QHORN.- 7.5.2 Folgerung und Äquivalenz.- 7.6 Quantifizierte 2-KNF-Formeln.- 7.7 Übungsaufgaben.- Algorithmenverzeichnis.- Symbolverzeichnis.


Klappentext



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.


Ähnliche Artikel