Burkhardt Renz

Logik und formale Methoden TI5002

Spezifizieren, Modellieren und Überprüfen von Systemen mittels angewandter Logik

Übersicht

Moodle-Kurs zur Veranstaltung ⇗

Materialien

Zitate zu Logik und formale Methoden.
Portable Document Format, 3127 KB, Stand 7.09.2019
Burkhardt Renz: Logik und formale Methoden. Vorlesungsskript Technische Hochschule Mittelhessen
Portable Document Format, 6220 KB, Stand 7.04.2021
Regeln des natürlichen Schließens.
Portable Document Format, 185 KB, Stand 9.11.2020
Tobias Völzel: Natürliche Deduktion in Clojure. Masterarbeit Technische Hochschule Mittelhessen, 2015
Portable Document Format, 1499 KB, Stand 25.05.2018
Burkhardt Renz: Natürliches Schließen in Coq - Ein einführendes Tutorial. Technische Hochschule Mittelhessen, 2019
Portable Document Format, 423 KB, Stand 29.01.2020
Burkhardt Renz und Nils Asmussen: Kurze Einführung in Alloy. Technische Hochschule Mittelhessen
Portable Document Format, 416 KB, Stand 25.10.2020
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 25.05.2018
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 25.05.2018
C. M. Sperberg-McQueen: Alloy 4 quick reference summary. Black Mesa Technologies LLC., 2013
Portable Document Format, 136 KB, Stand 25.10.2020
Burkhardt Renz: Model Checking mit SPIN - Beispiele. Vorlesungsskript Technische Hochschule Mittelhessen
Portable Document Format, 487 KB, Stand 20.01.2020
Quellen der Beispiele mit Alloy aus der Vorlesung.
Zip Archivdatei, 3 KB, Stand 25.05.2018

Übungen/Praktikum

Übungen zur Aussagenlogik.
Portable Document Format, 371 KB, Stand 8.10.2020
Übungen zur Prädikatenlogik.
Portable Document Format, 443 KB, Stand 22.12.2020
Übungen zur temporalen Logik.
Portable Document Format, 3238 KB, Stand 8.10.2020

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 25.05.2018
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.

Projektseite der LWB.

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.

Projektseite von Jape. ⇗

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 25.05.2018
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.

> Projektseite von Alloy. ⇗

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.

> Projektseite von Spin. ⇗

Am 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.