Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

 FB Inf

Automatisches Beweisen

Die Aufgabe beim (automatischen) Beweisen ist es, aus einer Menge von Fakten, den Axiomen, ein vorgegebenes Faktum, das Ziel, abzuleiten. Gelingt dies, ist das Ziel ein Theorem.
Es gibt die unterschiedlichsten Arten, wie man das "Ableiten" definieren kann, und zwar in Abhängigkeit davon, was man als Fakten zuläßt. Wir haben als Fakten Gleichungen gewählt, und unser Ableitungsbegriff ist das Anwenden dieser Gleichungen, um "Gleiches durch Gleiches zu ersetzen". Da die Platzhalter in unseren Gleichungen (wie z.B. x,y und z) beliebig ersetzt werden dürfen, sind sehr viele Ableitungen möglich, so daß ein sehr schweres Suchproblem entsteht.

Das untenstehende Bild zeigt einen von unserem Beweissystem DISCOUNT erstellten Beweis. Die englischen Einleitungen und die Aufteilung des Beweises in Zwischenziele (sog. Lemmata) wurden von DISCOUNT selbst erstellt. Der Teil eines Faktums, auf den eine Gleichung angewendet wird, ist jeweils unterstrichen und der neu eingefügte Teil ist fett gedruckt. Außerdem steht an jedem Schritt, welche Gleichung mit welcher Einsetzung für die Platzhalter angewendet wurde.
Hier geht es
Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!
Letzte Änderung: Wednesday, 26-Oct-05 08:59:21 GMT
www-aven@informatik.uni-kl.de