Logik und formale Methoden TI5002
Spezifizieren, Modellieren und Überprüfen von Systemen mittels angewandter Logik
Übersicht
Moodle-Kurs zur Veranstaltung ⇗
Materialien
 |
Burkhardt Renz: Logik und formale Methoden. Vorlesungsskript Technische Hochschule Mittelhessen Portable Document Format, 6274 KB, Stand 17.10.2023 |
|
Regeln des natürlichen Schließens. Portable Document Format, 185 KB, Stand 17.10.2023 |
|
Tobias Völzel: Natürliche Deduktion in Clojure. Masterarbeit Technische Hochschule Mittelhessen, 2015 Portable Document Format, 1499 KB, Stand 17.10.2023 |
|
Burkhardt Renz: Natürliches Schließen in Coq - Ein einführendes Tutorial. Technische Hochschule Mittelhessen, 2019-2024 Portable Document Format, 447 KB, Stand 31.03.2024 |
|
Burkhardt Renz und Nils Asmussen: Kurze Einführung in Alloy. Technische Hochschule Mittelhessen Portable Document Format, 416 KB, Stand 17.10.2023 |
|
Nils Asmussen: Einführung in Alloy. Präsentation (ohne Animation) Institut für
SoftwareArchitektur an der Fachhochschule Gießen-Friedberg Portable Document Format, 287 KB, Stand 17.10.2023 |
|
Nils Asmussen: Ansätze zur Modellierung von Dynamik mit Alloy. Technischer Bericht Nr. 1 des Instituts für
SoftwareArchitektur, September 2010 Portable Document Format, 511 KB, Stand 17.10.2023 |
|
C. M. Sperberg-McQueen: Alloy 4 quick reference summary. Black Mesa Technologies LLC., 2013 Portable Document Format, 136 KB, Stand 17.10.2023 |
|
Burkhardt Renz: Model Checking mit SPIN - Beispiele. Vorlesungsskript Technische Hochschule Mittelhessen Portable Document Format, 487 KB, Stand 17.10.2023 |
 |
Quellen der Beispiele mit Alloy aus der Vorlesung. Zip Archivdatei, 3 KB, Stand 17.10.2023 |
Übungen/Praktikum
|
Übungen zur Aussagenlogik. Portable Document Format, 389 KB, Stand 17.10.2023 |
|
Übungen zur Prädikatenlogik. Portable Document Format, 465 KB, Stand 17.10.2023 |
|
Übungen zur temporalen Logik. Portable Document Format, 3252 KB, Stand 17.10.2023 |
Werkzeuge
Logik in LaTeX
Eine umfassende Liste von Zeichen in LaTex, darunter auch die für die Logik benötigten findet man in The Comprehensive LaTeX Symbol List ⇗von Scott Pakin.
Für Herleitungen im natürlichen Schließen eignet sich logicproof -- Box proofs for propositional and predicate logic ⇗ von Alan Davidson. (Siehe auch: CTAN Topic logic ⇗ sowie LaTeX for Logicians ⇗ von Peter Smith.)
 |
Symbole für Logik in LaTeX. LaTeX Package, 1 KB, Stand 17.10.2023 |
LWB
Die Logic Workbench (LWB) ist eine Sammlung von Clojure-Funktionen für die Aussagen-, Prädikaten- und temporale Logik. LWB unterstützt insbesondere auch das natürliche Schließen.
Für LWB gibt es ein eine App, mit der man LWB recht einfach verwenden kann. Die App heißt lwb-gui und kann von Github geladen werden. Für die App ist Java 9 oder neuer erforderlich.
Ich habe lwb-gui auf MacOS getestet und verwende die App regelmäßig. Auf Windows und Linux wurden nur kurze Tests durchgeführt. Bitte Rückmeldung, wenn etwas nicht funktioniert.
Jape
Jape ist ein Werkzeug, mit dem man interaktiv Herleitungen des natürlichen Schließens entwickeln und/oder überprüfen kann.
Ich habe spezielle Anpassungen von Jape gemacht und auch die Aufgaben aus den Übungsblättern eingebaut:
|
Anpassungen von Jape für die Übungen. Zip Archivdatei, 29 KB, Stand 17.10.2023 |
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, 2012.
Spin
Spin ist ein Model Checker, jSpin eine Java-Oberfläche für Spin. Wir setzen Spin im Teil der Vorlesung über temporale Logik ein.
Am einfachsten installiert man Spin auf Basis der Distribution von jSpin von Moti Ben-Ari auf der
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.