Literatur und Folien
Diese Seite ist im Aufbau. Einige der verlinkten Foliensätze sind evtl. noch nicht aktuell!
Literatur
- Wolfgang Bibel: Deduktion -- Automatisierung der Logik, R.Oldenbourg, 1992. (Dieses Buch ist nicht mehr im Handel und kann als Postscriptfile heruntergeladen werden (Zugriff nur aus dem Netz der Universität Potsdam): W.Bibel: Deduktion -- Automatisierung der Logik)
- Lincoln Wallen: Automated deduction in nonclassical logics, MIT Press, 1990
- Raymond M. Smullyan: First-order logic, Dover, 1995.
- An Introduction to mathematical logic and Type Theory: To Truth through Proof. Kluwer, Applied Logic Series 27 2002
- Handbook of Automated Reasoning. Elsevier 2001
- Literatur zu den einzelnen Themengruppen wird separat vorgestellt.
-
Connection-based Theorem Proving in Classical and Non-classical Logics
- T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods
- Connection-Driven Inductive Theorem Proving
- Folien der Vorlesung
Einführung: | Vorlesung Inferenzmethoden im SS 2015 | pdf |
animiert |
||||
Teil I: Logik und Beweiskalküle | |||||||
Einheit 1 | Formale Logik | animiert | |||||
Einheit 2 | Tableauxkalküle | pdf |
animiert |
||||
Einheit 3 | Matrixbeweise | pdf |
animiert |
||||
Teil II: Deduktionsverfahren | |||||||
Einheit 4 | Die Konnektionsmethode |
pdf |
animiert |
||||
Einheit 5 | Unifikation |
pdf |
animiert |
||||
Einheit 6 | Das Extensionsverfahren für Nicht-Normalform-Matrizen |
pdf |
animiert |
||||
Einheit 7 |
Reduktions- und Optimierungstechniken |
pdf |
animiert |
||||
Einheit 8 | Exkurs: Bezug zu anderen Deduktionsverfahren | pdf |
animiert |
||||
Teil III: Konstruktion effizienter Theorembeweiser (entfällt 2015) |
|||||||
Einheit 9 | Implementierung von Beweiverfahren |
pdf |
|||||
Einheit 10 | Analyse von Beweisern / Problembibliotheken |
pdf |
|||||
Einheit 11 | Optimierungen und Erweiterungen |
pdf |
|||||
Teil IV: Jenseits von Prädikatenlogik | |||||||
Einheit 12 | Konstruktive Logik |
pdf |
animiert |
||||
Einheit 13 | Modallogiken |
pdf |
animiert |
||||
Einheit 14 | Logiken höherer Stufe |
pdf |
animiert |
||||
Teil V: Behandlung spezifischer Fragestellungen | |||||||
Einheit 15 | Theorie- und Gleichheitsbehandlung |
pdf |
animiert |
||||
Einheit 16 | Zahlen und Induktion |
pdf |
animiert |
||||
Einheit 17 | Termersetzungssysteme |
pdf |
animiert |
||||
Einheit 18 | Offene Themen |
pdf |
(Keine Animation) |