Automatische Synthese rekursiver Programme als Beweisverfahren von Susanne Biundo | ISBN 9783540553007

Automatische Synthese rekursiver Programme als Beweisverfahren

von Susanne Biundo
Buchcover Automatische Synthese rekursiver Programme als Beweisverfahren | Susanne Biundo | EAN 9783540553007 | ISBN 3-540-55300-2 | ISBN 978-3-540-55300-7

Automatische Synthese rekursiver Programme als Beweisverfahren

von Susanne Biundo

Inhaltsverzeichnis

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