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. Some of the links below are unfortunately broken. I would particularly welcome updates about these so that this page remains useful.

Accessible theorem provers

Aximo - a tool for verifying knowledge in dynamic multi-agent scenarios based on the algebraic axiomatics of dynamic epistemic logic. Implemented by Simon Richards and Mehrnoosh Sadrzadeh.
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 description logic OWL reasoner by Ian Horrocks and Dmitry Tsarkov. Successor of FaCT.
Gost - A Lisp implementation of a tableau algorithm for GF1-, a sublogic of the "First Guarded Fragment".
Herod and Pilate - Two tableau decision procedures for the hybrid logic HL(@) implemented by Marta Cialdea, Serenella Cerrito and their students. Based on internalized tableau calculi, without loop-checking and no restriction on the order of the application of the rules.
J-prover - A connection/matrix based prover that produces sequent proofs for FO-Intuitionistic, and propositional S4 and S4nJ logics, implemented as a module of the MetaPRL logical framework. Web interface for modal logic.
KtSeqC - A theorem prover for the minimal tense logic Kt.
LoTREC - A generic tableau theorem prover for modal logic, which is suitable for creating, testing and analysing tableau method implementations. Web interface
Logics Workbench (LWB) - A sequent based theorem prover for a range of propositional logics, including modal logics, temporal logics, intuitionistic logics and nonmonotonic logics. Web interface
MetTeL - a general tableau prover core allowing specifications of several, different tableau provers in a plug-in style. Implemented by Dmitry Tishkovsky.
MLTP - An efficient and generic modal logic tableau prover inplemented by Zhen Li.
ModLeanTAP - A lean implementation of a free variable tableau calculus for a range of propositional modal logics.
MOLTAP - An automated modal logic tableau prover for epistemic logics with various knowledge operators including the common knowledge operator. By Twan van Laarhoven.
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. The features of MSPASS are now incorporated in the latest release of SPASS. Web interface
pdl-tableau - A prototypical implementation of the tableau calculus for PDL. Implemented by Renate Schmidt. Web 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.) Web interface
pttf - A satisfiability checker for propositional temporal transition formulae developed by Anatol Ursu. Web interface
RACER - A description logic reasoner for the Semantic Web languages OWL/RDF.
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.
SPASS - A saturation-based resolution theorem prover for first-order logic with equality, sorted logic, and many non-classical logics including traditional style modal logics, dynamic modal logics, description logics and relational logics.
*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.
TRP - A protoypical implementation of a theorem prover for propositional linear-time logic based on the temporal resolution calculus.
TRP++ - A C++ implementation of a theorem prover for propositional linear-time logic based on the temporal resolution calculus.
TeMP - A C++ implementation of a theorem prover for the monodic fragment of first-order linear-time temporal logic over expanding domains based on the temporal resolution calculus.
TTM - A tableau-based theorem prover for temporal logic PLTL that also provides a model for satisfiable sets of PLTL-formulas.
Tableau WorkBench (TWB) - A generic framework for building automated theorem provers for arbitrary propositional logics, includig modal and temportal logics.

Translators

SPASS, 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. MSPASS Web interface
Axiomatic translation - An implementation of the axiomatic translation for a large class of modal axioms by John Kevin Smith. Web interface
PLTLmona - A translator from propositional linear-time logic to MONA input syntax.
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. Web 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. Web interface
SQEMA - Computes first-order equivalents and proves canonicity of modal formulas. Web interface

For the back-translation:

krachtweb - Computes modal axioms from Kracht formulae, with webinterface.

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.

ALC Problems - for ALC with non-empty TBox, generated and used for tests reported in Hustadt and Schmidt (1997, 1999).
LWB benchmark formulae - for the propositional modal logics K, KT, and S4.
TANCS 2000 Problems - TANCS was a competition of non-classical systems held in conjunction with TABLEAUX 1998 and 2000. See also problems used for tests with MSPASS.
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.