Tutorium zum interaktiven Beweisen in Isabelle/HOL

• Applicant: Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2000 to 2002
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants