Dieter Hofbauer, Ralf-Detlef Kutsche

Grundlagen des maschinellen Beweisens (eBook, PDF)

Eine Einführung für Informatiker und Mathematiker

• Format: PDF

Produktdetails

• Verlag: Vieweg+Teubner Verlag
• Seitenzahl: 172
• Erscheinungstermin: 8. März 2013
• Deutsch
• ISBN-13: 9783322842237
• Artikelnr.: 53386113

Inhaltsangabe

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.