×
Automatische Synthese rekursiver Programme als Beweisverfahren
von Susanne BiundoInhaltsverzeichnis
- 1. Einführung.
- 2. Übersicht.
- 3. Formale Grundbegriffe.
- 3.1 Syntaktische Grundbegriffe.
- 3.2 Semantische Grundbegriffe.
- 3.3 Theoriespezifikationen.
- 4. Beweis durch Synthese.
- 4.1 Der Synthesekalkül.
- 4.2 Korrektheit.
- 5. Transformationsregeln.
- 5.1 Induktionsregeln.
- 5.2 Normalisierung.
- 5.3 Termersetzungsregeln.
- 5.4 Fallunterscheidungsregeln.
- 5.5 Extraktionsregeln.
- 5.6 Implikationenregel.
- 5.7 Eliminationsregel.
- 6. Das Syntheseverfahren als Existenzbeweismethode.
- 6.1 Auswahl eines geeigneten Induktionsaxioms.
- 6.2 Konstruktion eines lösenden Terms.
- 6.3 Verwendung von Eigenschaften des lösenden Terms zum Beweis.
- 7. Die Mechanisierung des Verfahrens.
- 7.1 Die Struktur des Suchraumes.
- 7.2 Die Suchstrategie.
- 7.3 Die vier Phasen des Syntheseprozesses.
- 7.4 Die Zulässigkeit des synthetisierten Programmes.
- 8. Heuristiken.
- 8.1 Auswahl der Induktionsaxiome.
- 8.2 Symbolische Auswertung.
- 8.3 Verwendung von Induktionshypothesen.
- 8.4 Lösung von Konflikten.
- 8.5 Verwendung von Bedingungen.
- 8.6 Auswahl von Restformeln.
- 8.7 Bewertung von Regelanwendungen.
- 9. Beispiele.
- 9.1 Die Vollständigkeit eines Beweisers für Aussagenlogik.
- 9.2 Die Synthese einer Funktion zur Umkehrung von Listen.
- 9.3 Die Synthese einer Sortierfunktion.
- 9.4 Die Synthese von ganzzahligem Quotient und Rest.
- 10. Schlußbemerkungen.
- Literatur.
- Anhang A: Sorten, Stellen und Ordnungsrelationen.
- Anhang B: Verzeichnis der Symbole und Abkürzungen.