Webseite zur Vorlesung

Material

Vorlesungsunterlagen

• Das Skriptum zur Vorlesung
  Dieses Skriptum kann sich während der Vorlesungszeit noch etwas verändern.
• Die Folien der Vorlesung

Werkzeuge

• Der SAT-Solver MiniSat
• Das Verifikationswerkzeug KeY, das für interaktive prädikatenlogische Beweise genutzt werden wird
• Der LTL-Modelchecker SPIN, zu dem es vermutlich auch Aufgaben geben wird
• Visualisierung von Tableaubeweisen erlaubt interaktive Beweise im Tableaukalkül zu führen.

Literatur

• M. Fitting: First Order Logic and Automated Theorem Proving
• U. Schöning: Logik für Informatiker
• V. Sperschneider/G. Antoniou: Logic: a Foundation for Computer Science
• P.H. Schmitt: Theorie der logischen Programmierung
• Huth und Ryan: Logic in Computer Science
• Ehrig, Mahr et al: Mathematische Grundlagen der Informatik
• E. Börger: Logik, Berechenbarkeit, Komplexität
• Ebbinghaus/Flum/Thomas: Mathematische Logik
• R. Smullyan: First Order Logic
• B. Beckert, R. Hähnle, P. Schmitt: The KeY Approach
• OMG OCL-Spezifikation 2.0

Verweise

• Ein Java-Applet, das Sudoko auf ein SAT-Problem abbildet