|
|
|
|
|
|
Vorlesung Logik und formale Methoden MN5002
|
| 1 | Einführung |
| 1.1 | Zur Vorlesung |
| 1.2 | Logik und formale Methoden |
| 2 | Aussagenlogik |
| 2.1 | Aussagen |
| 2.2 | Die formale Sprache der Aussagenlogik |
| 2.3 | Die Semantik der Aussagenlogik |
| 2.4 | Beweissysteme der Aussagenlogik – Natürliches Schließen |
| 2.5 | Normalformen |
| 2.6 | Entscheidbarkeitsfragen der Aussagenlogik |
| 2.7 | SAT-Solver |
| 2.8 | Anwendungen in der Softwaretechnik mit MPA |
| 3 | Prädikatenlogik |
| 3.1 | Objekte und Prädikate |
| 3.2 | Die formale Sprache der Prädikatenlogik |
| 3.3 | Die Semantik der Prädikatenlogik |
| 3.4 | Beweissysteme der Prädikatenlogik – Natürliches Schließen |
| 3.5 | Normalformen |
| 3.6 | Unentscheidbarkeit der Prädikatenlogik |
| 3.7 | Ausdruckskraft der Prädikatenlogik |
| 3.8 | Anwendungen – Mikromodelle von Software mit Alloy |
| 4 | Temporale Logik |
| 4.1 | Zustände und Aussagen |
| 4.2 | Die formale Sprache der linearen temporalen Logik (LTL) |
| 4.3 | Die Semantik der LTL |
| 4.4 | Entscheidbarkeitsfragen der LTL |
| 4.5 | Anwendungen – Model Checking mit Spin |
In der Vorlesung werde ich mich sehr eng an das Buch
Michael Huth and Mark Ryan
Logic in Computer Science: Modelling and Reasoning about
Systems halten.
Es gibt viele gute Bücher über Logik, auch speziell für die Logik in der Informatik, einige Titel, die sich zur begleitenden Lektüre eignen, finden Sie hier.
 |
Klassische Zitate zur Logik. Portable Document Format, 128 KB, Stand 26.03.2009 |
|
Regeln des natürlichen Schließens. Portable Document Format, 162 KB, Stand 23.03.2009 |
|
Burkhardt Renz: Kurze Einführung in Alloy. Fachhochschule Gießen-Friedberg Portable Document Format, 299 KB, Stand 10.12.2009 |
 |
Quellen der Beispiele mit Alloy aus der Vorlesung. Zip Archivdatei, 3 KB, Stand 11.06.2009 |
|
Übungen zur Vorlesung. Portable Document Format, 400 KB, Stand 14.04.2009 |
MPA - MNI Proposition Analyzer.
Der MPA ist ein Werkzeug zur Analyse von Formeln der Aussagenlogik. Es kann zur Überprüfung eines Teils der Übungsaufgaben eingesetzt werden, sowie zu den Anwendungen im Teil der Vorlesung über die Aussagenlogik, insbesondere das Variabilitätsmodell für Softwareproduktlinien.
Alloy.
Alloy ist ein Model Finder, mit dem man Modelle von Software analysieren kann. Wir setzen Alloy im Teil der Vorlesung über die Prädikatenlogik ein.
Der Ansatz von Alloy wird in folgendem Buch beschrieben: Daniel Jackson Software Abstractions: Logic, Language, and Analysis MIT Press, 2006.
Spin und jSpin.
Spin ist ein Model Checker, jSpin eine Java-Oberfläche für Spin. Wir setzen Spin im Teil der Vorlesung über temporale Logik ein.
An einfachsten installiert man Spin auf Basis der Distribution von jSpin von Moti Ben-Ari auf der Projektseite von jSpin.
Der Ansatz von Spin und die Verwendung von jSpin wird in folgendem Buch beschrieben: Mordechai Ben-Ari Principles of the Spin Model Checker Springer, 2008.
|
|
|
|
|
|
|
© 2005 - 2009 |
[Aktuell] [Veranstaltungen] [Projekte & Publikationen] [Literatur & Links] [Miscellanea] [Impressum] [<][^][>] |
