Literatur: Logik, Semantik und Verifikation

Hauptseite
Literatur
Übungen
Klausuren
Mailingliste
Software
Material

Die wichtigsten Dinge aus der Vorlesung halte ich in einem Skript fest, dass online verfügbar ist. Neben dem Skript sollten sie unbedingt noch weitere Literatur studieren, weil das Skript in Bezug auf Motivation und Abdeckung noch recht dünn ist. Für Aussagen- und Prädikatenlogik empfehle ich das Buch von Schöning (Kapitel 1+2). Für Semantik von Programmiersprachen und Hoare-Logik empfehle ich das Buch von Winskel (Kapitel 1-7 und Anhang A). Interessant finde ich auch das Buch von Huth und Ryan, dass neben Aussagen- und Prädikatenlogik auch Model Checking und Modallogiken behandelt und sich durch eine besonders intuitive Darstellung auszeichnet. Oft werden Sie auch Dinge brauchen, die Sie bereits in der Vorlesung Programmierung gelernt haben.

Grundlegend

• Uwe Schöning, Logik für Informatiker, 5. Auflage. Spektrum Akademischer Verlag, 2000.
• Gert Smolka, Logik, Semantik und Verifikation, Vorlesungsskript SS 2001.
• Gert Smolka, Programmierung: Eine Einführung für Informatiker, Vorlesungsskript WS 2000.
• Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.
• Michael R. A. Huth und Mark D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2000.

Weiterführend

• Melvin Fitting, First-Order Logic and Automated Theorem Proving. Second edition, Springer-Verlag, 1996. Leider zur Zeit vergriffen.
• Jean H. Gallier, Logic for Computer Science. Foundations of Automatic Theorem Proving. Harper&Row, 1986.
• René Lalement, Computation as Logic. International Series in Computer Science, Prentice Hall, 1993.
• Steve Reeves and Michael Clarke, Logic for Computer Science. Addison-Wesley, 1990.
• Franz Baader and Tobias Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
• John C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.
• Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking. The MIT Press, 1999.