When a course instance has been created from a template, the course instance will be in this state
In diesem Seminar werden sowohl theoretische Grundlagen als auch aktuelle Techniken zur Realisation von interaktiven und automatischen Theorembeweisern für klassische Logik höherer Stufe (HOL) diskutiert. Theorembeweiser sind Programme, die eine Menge von Annahmen ("Axiome") und eine Behauptung annehmen und dann versuchen zu beweisen (oder zu widerlegen), dass die Behauptung eine logische Konsequenz der Annahmen ist. Theorembeweiser können z.B. zur Programmverfikation (beweise, dass bestimmte Zusicherungen gelten), zur Beweisassistenz (bestötige dass meine Beweisführung korrekt ist) und in weiteren Einsatzgebieten formaler Methoden verwendet werden. Ebenso ist durch jüngere Forschungsresultate bestätigt, dass insbesondere Theorembeweiser für Prädikatenlogik höherer Stufe für die Verfikation/Analyse von Argumenten aus der theoretischen Philosophie/Metaphysik eingesetzt werden können.
Was sind die mathematischen Grundlagen für solche Programme? Wie implementiert man diese (effizient)? Viele der Themen sind aktuelle Forschungsgegenstände und können in ambitionierte Bachelor- und Masterarbeiten münden. Die Veranstaltung ist für 15 Studierende ausgelegt.
Vortragsthemen können umfassen:
und weiteres
Zusätzliche Informationen: Die Veranstaltungsseite ist unter https://kvv.imp.fu-berlin.de/portal/site/55834098-fcdb-47ba-9fc6-e83a3c79236f/ erreichbar.
In this seminar, we discuss theoretical and practical aspects of interactive and automated theorem proving in classical higher-order logic (HOL). Many of the discussed topics are currently of research interest and can lead to ambitious master's theses.
Possible topics include:
The page of the event is available here
Literatur: Wird auf der Veranstaltungsseite bekanntgegeben.