Direkt zum Inhalt | Direkt zur Navigation

Sektionen
Benutzerspezifische Werkzeuge

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.
  • Peter B. Andrews: An Introduction to mathematical logic and Type Theory: To Truth through Proof. Kluwer, Applied Logic Series 27 2002
  • A. Robinson & A. Voronkov: Handbook of Automated Reasoning. Elsevier 2001
  • Literatur zu den einzelnen Themengruppen wird separat vorgestellt.
  1. Connection-based Theorem Proving in Classical and Non-classical Logics
  2. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods
  3. 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 pdf 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)

 

Artikelaktionen
Auf einen Blick
Lehrform Vorlesung/Übung
Empfohlen ab FS 2
Voraussetzungen Logikvorkenntnisse sind erforderlich.
Benotet Ja
Punkte gesamt 6
davon praktisch 0
Sprache deutsch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000), Wahlfrei(7000)
Studiengang Bachelor, Master
Belegung via PULS