Tutorium zum interaktiven Beweisen in Isabelle/HOL

点击翻译按钮获取中文摘要

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.