Angewandte Beweistheorie: MINLOG

Die Beweisumgebung MINLOG wird von den Beweistheoretikern an der LMU entwickelt mit dem Anspruch, weitgehende logische Flexibilität zu bieten. Dabei orientiert sich der Entwicklungsbedarf auch an aus der Industrie angeregten Fallstudien. Aufgrund der theoretischen Fundierung ist MINLOG ein Werkzeug zur garantiert fehlerfreien Programmierung.

Im Kern ist MINLOG ein interaktiver Theorembeweiser für das tex2html_wrap_inline45-Fragment der Minimallogik über berechenbaren Funktionalen höheren Typs. Beweise werden im Natürlichen Schließen in der Regel zielorientiert geführt und via Curry-Howard Isomorphismus im lambda-Kalkül notiert. Objekt- und Beweisterme werden durch Auswertung normalisiert, Terme mit gleicher Normalform identifiziert. Durch Eingabe von Termersetzungsregeln kann man die Zahl der Interaktionen reduzieren. Ein schneller automatischer Beweiser erledigt logische Schlüsse.

Klassische Beweise von tex2html_wrap_inline45-Formeln können mit Friedmans Trick in konstruktive transformiert werden. Goads Beschneidungstechnik führt zur Vereinfachung von Beweisen in Spezialfällen. Kreisels modifizierte Realisierbarkeits-Interpretation verwandelt den Beweisterm einer tex2html_wrap_inline45-Formel in ein diese als Spezifikation erfüllendes SCHEME-Programm.

MINLOG bietet eine schlanke Theorie und ist offen für Erweiterungen. Die Manipulation von Beweistermen beherrschen sonst nur viel komplexere typentheoretische Systeme. - Fazit: MINLOG ist angewandte Beweistheorie pur.


1.7.1999, Wolfgang Zuber