Tutorium zum interaktiven Beweisen in Isabelle/HOL

• Antragsteller: Professor Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2000 bis 2002
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5273368

Ziel des Forschungsvorhabens ist die Erstellung eines zum interaktiven Beweisen in höherstufiger Logik am Beispiel des Theorembeweisens Isabelle/HOL. Es gibt zu diesem Gebiet zur Zeit nur sehr wenig Literatur, und diese ist dann oft sehr systemspezifisch oder implementierungsnah angesiedelt. Dies stellt eine erhebliche Hürde für das Erlernen der Benutzung von Theorembeweisern dar. Zusammen mit Dr. Paulson in Cambridge wird der Antragsteller ein Tutorium schreiben, das diese Hürde beseitigt, indem es sowohl die allgemeinen Beweisprinzipien höherstufiger Logik erläutert als auch in en Gebrauch des Systems Isabelle/HOL einführt. Zielpublikum sind Informatiker und Mathematiker, denen die Grundprinzipien der funktionalen Programmierung vertraut sind. Insbesondere wird es sich an den Anforderungen der universitären Ausbildung orientieren.

• DFG-Verfahren: Sachbeihilfen