Bachelorarbeit "Interaktiver Beweisassistent für höherstufige Logik"

Saarland University
Computer Science
Programming Systems
People

Downloads

Bachelorarbeit (pdf)

Christian Hümbert, Betreuer: Gert Smolka

Motivation

Formale mathematische Beweise zu führen ist eine nichttriviale Angelegenheit. Zum einen sind viele Studenten mit dem mathematischen Formalismus nicht vertraut, zum anderen ist die Fehleranfälligkeit bei der Durchführung formaler Beweise sehr hoch.
Hier können "Beweisassistenz-Systeme" den Benutzer unterstützen. (Bekannte Systeme sind: ACL2, PVS, LEGO, Isabelle )
Die Software ist nicht in der Lage, einen Beweis automatisch zu führen, vielmehr muss der Benutzer an den vom System zur Eingabe auffordernden Stellen die richtigen Entscheidungen treffen, um den Beweis korrekt abschließen zu können. Dabei prüft das System jeden Beweisschritt auf syntaktische und semantische Korrektheit.

Aufgabenstellung

Im Rahmen dieser Bachelorarbeit soll ein interaktives Beweistool für prädikatenlogische Formeln höherer Stufe (HOL) designt und implementiert werden.
Dieses System wird auf dem einfach getypten Lamda-Kalkül (S) und den Regeln des natürlichen Schließens, einem Deduktionssystem, das 1934 von Gerhard Gentzen entwickelt wurde, aufbauen. (s. References Kap. 11 Prädikatenlogik, Seite 5 Abb. 11.2)
Es wird einen Interpreter geben, der in drei Phasen arbeitet:

Declarative Phase
Hier werden neue Typen und Konstanten definiert, sowie das zu beweisende Theorem in Form einer HOL-Formel ("goal").
Prooving Phase
Mithilfe weniger Kommandos und geeigneten Variableninstanziierungen sollte es dann moeglich sein, den Beweis zu führen. Während des Beweisvorgangs kann es vorkommen, dass Lemmata "abgespalten" werden und ebenfalls bewiesen werden müssen ("subgoals"). Um zum "goal" zu gelangen, müssen dann zuvor alle "subgoals" erreicht worden sein.
Documentation Phase
Wurde ein Beweis korrekt geführt, so kann dieser als Latex-File exportiert und nachvollzogen werden.

Das System soll nicht zwingend effizient, vielmehr einfach und kompakt sein, so dass es für Studenten, die sich mit Prädikatenlogik befassen (beispielsweise im Rahmen der Vorlesung ICL) nützlich ist.

References

R.David, C.Rafalli, An experiment concerning mathematical proofs on computers with French undergraduate students, Journal of applied logic, 2004
G.Smolka, Introduction to Computational Logic, Skript Kapitel 11 - Prädikatenlogik , 2004
K.H. Bläsius und H.J. Bürckert. Deduction Systems, Oldenburg-Verlag, 1989
G.Gentzen. Untersuchungen über das Logische Schließen. Mathematische Zeitschrift, 39:176-210, 405-431, 1935
C.P. Wirth. Descente Infinie + Deduction, Logic Journal of the IGPL, 12:1-96, 2004
C. Benzmüller und M.Kohlhase. Extensional Higher-Order Resolution. Proceedings of the 15th International Conference on Automated Deduction (CADE), LNAI vol. 1421, pp. 56-71, Lindau, Germany, 1998. Springer
A. A. Adams und L. A. Dennis. Rippling in PVS. Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics, pp. 84 - 91, 2003
M. Kaminski. Studies in Higher-Order Equational Logic. Bachelorarbeit, 2005
T. Nipkow, L.C.Paulson und M. Wenzel. Isabelle/HOL - A proof Assistant for Higher-Order Logic, Springer-Verlag, 2002. Lecture Notes in Computer Science No. 2283
N. Shankar, S. Owre, J. M. Rushby und D. W. J. Stringer-Calvert.PVS Prover Guide, 2001
D. Aspinall with T.Kleymann.Adapting Proof General, 2004

Christian Hümbert, 2005