AiML: Tools

In recent years the number of computational tools useful for modal logics, and related logics, has increased significantly, and is continuously increasing. The following is an incomplete list of

Accessible theorem provers
Translators
Automated correspondence theory
Visualisation
Generators of formulae
Collections of problems
Related links

Your contribution

If you'd like something added or changed please let Renate Schmidt (schmidt@cs.man.ac.uk) know.

Accessible theorem provers

BLIKSEM - Hans de Nivelle's resolution based theorem prover for modal logic and first-order logic with equality.
DLP - An experimental tableaux-based inference system by Peter Patel-Schneider for a range of description logics.
FaCT - A tableaux-based inference system by Ian Horrocks for a range of description logics. Accepts also modal syntax.
Gost - A Lisp implementation of a tableau algorithm for GF1-, a sublogic of the "First Guarded Fragment".
KtSeqC - A theorem prover for the minimal tense logic Kt.
Logics Workbench (LWB) - A sequent based theorem prover for a range of propositional logics, including modal logics, temporal logics, intuitionistic logics and nonmonotonic logics. WWW interface
ModLeanTAP - A lean implementation of a free variable tableau calculus for a range of propositional modal logics.
Molle - A cross-platform prover written in Java that implements Fitting's 1969 semantic tableaux algorithm for propositional modal logic. It can prove the validity of modal formulae and generate (counter-)models.
MSPASS - An enhancement of the first-order theorem prover SPASS with a translator of modal formulae and formulae of the relational calculus into first-order logic with equality. WWW interface
ptl - A propositional temporal logic (PTL) tautology checker developed by Geert Janssen at Eindhoven University of Technology. (28/03/2005: It seems that this tool is no longer available on-line.) WWW interface
pttf - A satisfiability checker for propositional temporal transition formulae developed by Anatol Ursu. WWW interface
RACER - A knowledge representation system that implements a highly optimized ABox tableaux calculus for an expressive description logic, called ALCQHIR+.
Saga - A Lisp program implementing a tableau algorithm for the Guarded Fragment of Predicate Logic.
Saturate - An experimental theorem prover for first-order logic, primarily based on saturation. It includes a translator for modal logic into first-order logic by semantic embedding.
*SAT - An experimentation platform of SAT-based decision procedures for expressive description logics, modal and temporal logics.
STeP - The Stanford Temporal Prover, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems.

Translators

MSPASS - Can be used as a translator of modal formulae, formulae of description logics, and formulae of the relational calculus into first-order logic with equality. Various standard and non-standard translations are available. WWW interface
Small collection of useful code - including SICStus Prolog code for the functional translation of modal formulae, SICStus Prolog code for simplifying modal formulae. Written for an empirical analysis of decision procedures for modal logic.

Automated correspondence theory

These tools are useful for computing correspondence properties:

The DLS Algorithm - A general tool for the elimination of second-order quantifiers, based on Ackermann's Lemma. WWW interface - Example, for axiom schema T:
exists P (-( all x (P(x) -> (exists y (R(x,y) & P(y))))))
SCAN - A general tool for the elimination of second-order quantifiers, based on resolution. Accepts also modal syntax. WWW interface
SQEMA - Computes first-order equivalents and proves canonicity of modal formulas. WWW interface

Visualisation

Logic Animations - a collection of JavaScript programs used for teaching of basic mathematical logic.

Generators of formulae

LISP code for randomly generating CNF formulae of multi-modal K - implemented by Ullrich Hustadt.
Generators are distributed together with some provers, e.g. FaCT and DLP.
TANCS Benchmarks Generators - implemented in C by Fabio Massacci and Francesco Donini. See also TANCS.

Collections of problems

The collection of modal problem sets is beginning to grow rapidly. The webpages of some provers above also have links to benchmark collections.

LWB benchmark formulae - for the propositional modal logics K, KT, and S4.
TANCS Problems - TANCS is a Non Classical System Comparison held regularly in conjunction with the TABLEAUX Conferences.
Multi-agent modelling in the Logics Workbench - A small number of implementations of situations, problems and reasoning in multi-agent systems, using epistemic logics.

Also of interest: Benchmark formulae for intuitionistic propositional logic.