Inhalt
1 Grundbegriffe der Prädikatenlogik.- 1.1 Syntax der Prädikatenlogik.- 1.2 Semantik der Prädikatenlogik.- 1.3 Normierung der Syntax: Gentzenformeln und die Schnittregel.- 1.4 Normierung der Semantik: Herbrand-Strukturen.- 1.5 Korrektheit und Vollständigkeit.- 1.6 Theorembeweisen durch Widerlegungen.- 2 Resolution.- 2.1 Unifikation.- 2.2 Resolution und Faktorisierung.- 3 Einschränkung des Suchraums.- 3.1 Der Suchraum.- 3.2 Allgemeine Konzepte.- 3.3 Strukturelle Konzepte.- 3.4 Ordnungskonzepte.- 3.5 Semantische Konzepte.- 3.6 Kombination von Konzepten.- 4 Repräsentation des Suchraums.- 4.1 Connection-Graph-Resolution.- 4.2 Matrix-Verfahren.- 4.3 Tableau-Verfahren.- 5 Paramodulation.- 5.1 Gleichheit.- 5.2 Paramodulation.- 6 Termersetzung: Grundlagen.- 6.1 Termersetzungssysteme.- 6.2 Ersetzungssysteme: Termination und Konfluenz.- 6.3 Lokale Konfluenz und kritische Paare.- 7 Termersetzung: Spezielle Techniken.- 7.1 Terminationskriterien.- 7.2 Knuth-Bendix-Vervollständigung.- 7.3 Induktive Beweise.- 7.4 Lösen von Gleichungen: Narrowing.- 7.5 Beweisen in speziellen Gleichheitstheorien.- Schlußbemerkungen.- Literatur.- Symbolverzeichnis.- Sachwortverzeichnis.
1 Grundbegriffe der Prädikatenlogik.- 1.1 Syntax der Prädikatenlogik.- 1.2 Semantik der Prädikatenlogik.- 1.3 Normierung der Syntax: Gentzenformeln und die Schnittregel.- 1.4 Normierung der Semantik: Herbrand-Strukturen.- 1.5 Korrektheit und Vollständigkeit.- 1.6 Theorembeweisen durch Widerlegungen.- 2 Resolution.- 2.1 Unifikation.- 2.2 Resolution und Faktorisierung.- 3 Einschränkung des Suchraums.- 3.1 Der Suchraum.- 3.2 Allgemeine Konzepte.- 3.3 Strukturelle Konzepte.- 3.4 Ordnungskonzepte.- 3.5 Semantische Konzepte.- 3.6 Kombination von Konzepten.- 4 Repräsentation des Suchraums.- 4.1 Connection-Graph-Resolution.- 4.2 Matrix-Verfahren.- 4.3 Tableau-Verfahren.- 5 Paramodulation.- 5.1 Gleichheit.- 5.2 Paramodulation.- 6 Termersetzung: Grundlagen.- 6.1 Termersetzungssysteme.- 6.2 Ersetzungssysteme: Termination und Konfluenz.- 6.3 Lokale Konfluenz und kritische Paare.- 7 Termersetzung: Spezielle Techniken.- 7.1 Terminationskriterien.- 7.2 Knuth-Bendix-Vervollständigung.- 7.3 Induktive Beweise.- 7.4 Lösen von Gleichungen: Narrowing.- 7.5 Beweisen in speziellen Gleichheitstheorien.- Schlußbemerkungen.- Literatur.- Symbolverzeichnis.- Sachwortverzeichnis.
Titel
Grundlagen des maschinellen Beweisens
Untertitel
Eine Einführung für Informatiker und Mathematiker
EAN
9783322842237
Format
E-Book (pdf)
Hersteller
Genre
Veröffentlichung
08.03.2013
Digitaler Kopierschutz
Wasserzeichen
Dateigrösse
13.74 MB
Anzahl Seiten
172
Auflage
1989
Lesemotiv
Unerwartete Verzögerung
Ups, ein Fehler ist aufgetreten. Bitte versuchen Sie es später noch einmal.