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
Bei Fragen, Problemen oder Anregungen bitte E-mail an
denzinge@informatik.uni-kl.de