Grundlagen des maschinellen Beweisens Eine Einführung für Informatiker und Mathematiker
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | German |
| Published: |
Wiesbaden
Vieweg+Teubner Verlag
1991, 1991
|
| Edition: | 2nd ed. 1991 |
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- l 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