Grundlagen des maschinellen Beweisens

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