Schlußbemerkungen

Zusammenfassung

In dieser Arbeit ist eine Methode vorgestellt worden, mit der Induktionsbeweise von Existenzaussagen automatisch geführt werden können. Sie beruht auf der Synthese von konstruktiven Definitionen für Skolemfunktionen.

Die synthetisierten Funktionsdefinitionen werden als rekursive Programme formuliert, so daß diese Beweismethode zugleich ein deduktives Programmsyntheseverfahren darstellt.

Basierend auf dieser Methode wurde ein System entwickelt, das vollautomatisch rekursive Programme erzeugt. Es arbeitet mit einer statischen 4-Phasen-Strategie, die den Transformationsprozeß grob vorschreibt. Sie garantiert, daß die synthetisierten Programme korrekt sind bzgl. ihrer Spezifikation, vorausgesetzt, die zusätzlich erzeugten Verifikationsbedingungen können bewiesen werden.

Zahlreiche Heuristiken steuern die Anwendung der Transformationsregeln innerhalb der einzelnen Phasen und sorgen dafür, daß in vielen Fällen auch der kürzeste Lösungsweg gefunden wird.