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, 3051 KB, Stand 25.05.2018
Burkhardt Renz: Logik und formale Methoden. Vorlesungsskript Technische Hochschule Mittelhessen
Portable Document Format, 629 KB, Stand 25.05.2018
Regeln des natürlichen Schließens.
Portable Document Format, 185 KB, Stand 25.05.2018
Tobias Völzel: Natürliche Deduktion in Clojure. Masterarbeit Technische Hochschule Mittelhessen, 2015
Portable Document Format, 1499 KB, Stand 25.05.2018
Burkhardt Renz und Nils Asmussen: Kurze Einführung in Alloy. Technische Hochschule Mittelhessen
Portable Document Format, 415 KB, Stand 4.06.2018
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, 135 KB, Stand 23.06.2018
Burkhardt Renz: Model Checking mit SPIN - Beispiele. Vorlesungsskript Technische Hochschule Mittelhessen
Portable Document Format, 485 KB, Stand 22.01.2019
Quellen der Beispiele mit Alloy aus der Vorlesung.
Zip Archivdatei, 3 KB, Stand 25.05.2018

Übungen/Praktikum

Übungen zur Aussagenlogik.
Portable Document Format, 373 KB, Stand 25.05.2018
Übungen zur Prädikatenlogik.
Portable Document Format, 441 KB, Stand 25.05.2018
Übungen zur temporalen Logik.
Portable Document Format, 1011 KB, Stand 25.05.2018

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 Plugin für Atom, mit dem man LWB recht einfach verwenden kann. Das Plugin heißt lwb-ui und steht im Package-Repositiory von Atom bereit.

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.

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.