General information
Zeitraum/Time Winter 2016/2017, first seminar session on 20.10.2016
Termine/Dates Donnerstag/Thursday, 14:00 - 16:00Raum/Room Takustr. 9 ("Institut für Informatik"), Seminarraum 051/room 051
Vorbesprechung/preparatory meeting Vorbesprechung am/preparatory meeting on 06.10.2016, 14-16 Uhr, Takustr. 9, SR051
Zielgruppe/Target audience Bachelor and master students of computer science and mathematics with interest in logics, automated reasoning and deduction systems
Module/Modules This seminar can be used as Proseminar (bachelor students) and as Seminar (for master students). See here for a complete list of modules to this seminar.
Eintrag im VV der FU Berlin/Entry at FU course catalouge VV Entry
Inhalt
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.
Topic
In this seminar, we discuss theoretical and practical aspects of interactive and automated theorem proving in classical higher-order logic (HOL). Theorem provers are computer programs that take a number of assumptions ("axioms") and a conjecture and then try to prove/refute that the conjecture is indeed a logical consequence of the given assumptions. Theorem provers can be employed in various disciplines of mathematics and computer science, e.g. for program verfication (prove that some assertion holds), for proof assistance (verify that my own proof is correct) and other fields of formal methods. Recent research also suggests that especially theorem provers for higher-order logic can be employed for verifying/analyzing arguments from theoretical philosophy/metaphysics.
What are the mathematical foundations for such programs? How can they be implemented (efficiently)? Many of the discussed topics are currently of research interest and can lead to ambitious bachelor's and master's theses.
Vortragsthemen/Topics for talks
Eine Liste von möglichen Vortragsthemen ist unter Talks/Vorträge (links im Menü) zu finden.
A preliminary list on possible topics for talks can be found at Talks/Vorträge (in the left navigation bar).
Weitere Infos/Further information
Literaturhinweise können unter Literature/Literatur (links im Menü) gefunden werden.
The course's literature is listed under Literature/Literatur (in the left navigation bar).