Logik-Software / Logik-Software für Unterrichtszwecke

Gandalf Theorem Prover for classical 1-st order logic
Tanel Tammet, Chalmers University of Technology, Schweden
online verfügbar
Gateway to Logic Interaktives Konstruieren von aussagenlogischen Herleitungen, Prüfung prädikatenlogischer Herleitungen (Kalkül des natürlichen Schließens)
Christian Gottschall, Universität Wien
online nutzbares Programm (deutsch und englisch), erfordert für einige Funktionen einen Java-fähigen Browser
Isabelle A Generic Theorem Prover, unterstützt eine große Anzahl von Logiken
deutsche Quelle: TU München
Jape Interaktives Werkzeug zur Konstruktion von Beweisen verschiedener Logiksysteme, deren Syntax und Schlußregeln in Jape codiert werden können
Richard Bornat, London & Bernard Sufrin, Oxford
online verfügbar
Logics Workbench Klassische und nicht-klassische Aussagenlogik (intuitionistische Logik, Modallogik, temporale Logik, nichtmonotone Logik)
Universität Bern, Schweiz
online verfügbar
Mechanized Reasoning
Systems
Database of Existing Mechanized Reasoning Systems
M. Kohlhase & C. Talcott, Stanford University, USA
Metamath Solitaire Interaktive Konstruktion von Beweisen in Logik und Mengenlehre
Norman D. Megill
Java Applet
Porgi Proof-Or-Refutation Generator for Intuitionistic propositional logic
Allen Stoughton, Kansas State University, USA
online verfügbar
P-Prover A Theorem Proving System for CLC (sequent style classical predicate logic)
KAKEHI Laboratry, Waseda University, Japan
online ausführbar
3TAP Tableau-based Theorem prover
Bernhard Beckert, Universität Karlsruhe
online verfügbar
WinWWT-Tool Überprüfung logischer Terme auf Gültigkeit mittels Wahrheitswerte-Tabellen. Die Bezeichnung der logischen Funktionen und ihre Bewertung können frei gewählt werden. Das Programm eignet sich daher nicht nur für die klassische Logik, sondern auch für jedes andere Logiksystem (dreiwertige Logik, intuitionistische Logik etc.).
PC/Win


 

Logik-Software für Unterrichtszwecke

Bertrand Testet Formeln der Aussagenlogik und der Prädikatenlogik 1. Stufe auf Erfüllbarkeit, Gültigkeit und Äquivalenz mittels Wahrheitstafeln und eines Baumtests nach dem Buch Deductive Logic von Hugues Leblanc und William A. Wisdom.
Mac, Demoversion verfügbar
CSLI:
Tarski's World
Programm zur Einführung in die Sprache der Logik 1. Stufe
auch Bestandteil des Logik-Buches The Language of First-order Logic von Jon Barwise und John Etchemendy
Mac und PC/Win
CSLI:
Hyperproof
Programm zur Einübung in das analytische Denken und die Konstruktion von Beweisen
ergänzt Tarski's World, Buch & Software von Jon Barwise und John Etchemendy
Mac
CSLI:
Turing's World
Simulation von Turing-Maschinen auf dem Computer
Buch & Software von Jon Barwise und John Etchemendy zur Einführung in Schlüsselbegriffe der Berechenbarkeitstheorie
Mac
Gibbins Beweisprüfer Interaktiver Beweisprüfer für den Kalkül des natürlichen Schließens nach  E. J. Lemmons Beginning Logic und für die Quantorenlogik nach Peter Gibbins Particles and Paradoxes
Java Applet
LogicCoach Programm zur Prüfung von Lösungen für Übungsaufgaben, in Verbindung mit dem Buch A Concise Introduction to Logic (Wadsworth) von Patrick Hurley; weitere Informationen zu LogicCoach: http://tcw2.ppsw.rug.nl/~hans/logiccoach. Das Programm kann direkt vom Autor Nelson Pole per Email-attachment bezogen werden: n.pole@csuohio.edu.
Mac und PC
Logic with Symlog Buch & Software von Frederic D. Portpraro und Robert E. Tully zur Einführung in die Satz- und Prädikatenlogik erster Stufe
Prentice Hall 1993
PC/DOS
MacLogic Beweisassistent für verschiedene Logiken erster Stufe (Kalkül des natürlichen Schließens, Sequenzkalküle)
University of St Andrews
Mac, Demoversion verfügbar
The Logic Daemon Programm zur Prüfung von Beweisen (Satz- und Prädikatenlogik) in Verbindung mit dem Buch Logic Primer (MIT Press 1992) von Colin Allen und Michael Hand
online
The LogicWorks Übungsprogramm für Logik-Grundkurs (Satz- und Prädikatenlogik)
Instructor Package ist kostenlos
Mac oder PC/DOS
Truth Table Practice Wahrheitstafeln vervollständigen
Antwort wird auf Korrektheit getestet
online

Jochen Lechner
lechner@phil-fak.uni-duesseldorf.de
Letzte Änderung: 22. Juli 1999