v
Bonn Mathematical Logic Group

Hauptseminar Mathematische Logik (S2A2): Praktische Logik


Dozenten

Termin

Übungen

Beschreibung


Die mathematische Logik zeigt, dass sich mathematisches Beweisen prinzipiell
durch formale Manipulationen von Formeln und Termen erfassen lässt. In der
"praktischen Logik" werden diese Manipulationen konkret realisiert. Die
Reduktion von nichttrivialen Aussagen und Beweisen auf logische
Elementarschritte führt zu großen Schrittzahlen und hohen Komplexitäten und
verlangt den Einsatz von Computern. Das Buch "Handbook of Practical Logic
and Automated Reasoning" von John Harrison (Cambridge University Press,
2009) ist eine Einführung in die mathematische Logik, die die Grundbegriffe
der Logik wie "Term", "Aussage", "formale Ableitung" usw. zugleich in
einer Programmiersprache implementiert. Dies führt zu funktionierenden
Programmen, mit denen Aussagen überprüft und generiert werden können. Die
Implementierung formaler Ableitungen liefert unmittelbar automatische
Beweiser, wie sie im Prinzip in modernen automatischen Theorembeweisern
eingesetzt werden. Hierfür benutzt Harrison die Programmiersprache OCaml
geschickt so, dass die Programme den Definitionen in der mathematischen Logik
ähneln.

In dem Seminar wollen wir uns vor allem mit den Kapiteln 2 - Propositional
Logic und 3 - First-Order Logic des "Handbooks" befassen. Das Seminar ist
als Ergänzung zur grundlegenden mathematische Logik gedacht - für
interessierte Hörer/innen der "Einführung in die Mathematische Logik",
"Mengenlehre" o.ä. Die Seminarvorträge stellen die logischen Begriffe
zunächst theoretisch, aber noch detaillierter als in der Logik-Vorlesung dar.
Dies ermöglicht ihre Umsetzung in OCaml. Die Programme stehen lauffertig auf
den Internetseiten von John Harrison zur Verfügung, sodass ein eigenes
Programmieren nicht notwendig ist. Die Programme erlauben verschiedene
Experimente, auch mit Veränderungen des Codes. Das soll auch während der
Seminarsitzungen geschehen, wobei die technische Durchführung (Laptops oder
Computerpool) zu Anfang des Sommersemesters besprochen werden wird.

Vorträge


28.04.14. Syntax und Semantik der Aussagenlogik (2.1-2.4): Annika Pick, Anna Ribelles, Timo Weiss; Thesenpapier 1
05.05.14. Normalformen: NNF, DNF und CNF (2.5-2.6, 2.8): Annika Pick, Anna Ribelles, Timo Weiss; Thesenpapier 2
12.05.14. Davis-Putnam-Verfahren (2.9): Jakob Jentgens, Uli Matzner, Jakob Speer
19.05.14. Stalmarck-Verfahren und binäre Entscheidungsdiagramme (2.10-2.11): Jakob Jentgens, Uli Matzner, Jakob Speer
26.05.14. Syntax und Semantik der Logik 1. Stufe (3.1-3.4): Payam Kamali, Emirhan Temur
16.06.14. PNF und Skolemisierung (3.5-3.6): Payam Kamali, Emirhan Temur
23.06.14. Herbrandmodelle und der Satz von Herbrand (3.7-3.8): Peter Neubert
30.06.14. Unifikation (3.9; evtl. 3.10): Leona Schlöder
07.06.14. Resolution (3.10; evtl. 3.11-3.12): Jendrik Stelzner
14.07.14. Horn-Klauseln und Prolog (3.14-3.15): Aras Ergus

Literatur


Harrison, James: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009).
Sheeran, Mary and Stalmarck, Gunnar: A tutorial on Stalmarck's proof procedure for propositional logic.

Installation


Installation unter Ubuntu:
1. Download OCaml gemäss Instruktionen.
2. Download Camlp5 (camlp5.5-6.11.tgz), vorzugsweise im selben Verzeichnis wie OCaml. Installation gemäss Anleitung in der INSTALL-Datei.
3. Download des Programmcodes von Harrison
4. (optional) Um OCaml mit Emacs zu verwenden: Installation von "tuareg-mode für Emacs" vom Software-Center. Alternativ: manuelle Installation

Verwendung des tuareg-mode für Emacs:
1. Emacs starten und tuareg-mode mit Alt-x aufrufen.
2. Das Verzeichnis, wo der Programm-Code von "Practical Logic and Automated Reasoning" gespeichert ist, öffnen.
3. Öffnen der Datei "init.ml" und mit Ctl-c Ctl-b kompilieren.
Beachte: vor der Benutzung anderer Dateien immer zuerst "init.ml" laden!

Verwendung unter Windows: mit einer Virtual machine.