WiSe 16/17  
19324417  
19324417 Seminar/Proseminar

WiSe 16/17: Seminar/Proseminar: Higher-Order Theorem Proving

Alexander Steen, Max Peter Wisniewski

Zusätzl. Angaben / Voraussetzungen

Zusätzliche Informationen: Die Veranstaltungsseite ist unter https://kvv.imp.fu-berlin.de/portal/site/55834098-fcdb-47ba-9fc6-e83a3c79236f/ erreichbar.

Schließen

Kommentar

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:

  • Einfach getypter Lambda-Kalkül: wichtigste theoretische Eigenschaften, sowie Beispiele (z.B. Church Numerals, ...);
  • Einführung in die Logik höherer Stufe (HOL): Historie und Abgrenzung, Syntax, Semantik;
  • Kalküle, Korrektheit, Vollständigkeit;
  • Cut-Elimination, Cut-Simulation;
  • Unifikation, Pre-Unifikation;
  • Skolemisierung, Normalformen;
  • Transformationen in Logik erster Stufe;
  • Implementierungstechniken (Indexing, Selektionsheuristiken, ...);

und weiteres

Schließen

Literaturhinweise

Literatur: Wird auf der Veranstaltungsseite bekanntgegeben.

16 Termine

Zusätzliche Termine

Do, 06.10.2016 14:00 - 16:00
Vorbesprechung

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Regelmäßige Termine der Lehrveranstaltung

Do, 20.10.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 27.10.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 03.11.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 10.11.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 17.11.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 24.11.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 01.12.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 08.12.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 15.12.2016 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 05.01.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 12.01.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 19.01.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 26.01.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 02.02.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 09.02.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Do, 16.02.2017 14:00 - 16:00

Dozenten:
Max Peter Wisniewski
Alexander Steen

Räume:
051/T9 Seminarraum (Takustr. 9)

Studienfächer A-Z