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
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
- ALCI prover - Graph-based tableau prover for description logic ALC with inverse roles also known as propositional mutimodal Kt written in Ocaml. By group of Rajeev Gore.
- BDDBiKt provers - Two implementations of provers for testing satisfiability, falsifiability and validity for propositional bi-intuitionistic tense logics, plus randomly generated formulae of intuitionistic logic. By group of Rajeev Gore.
- BiInt - A theorem prover for propositional bi-intuitionistic logic written by Linda Postniece.
- CardKt, CardS4, CardTAP - Theorem Provers on Java Smartcards by
Rajeev Gore with Phuong The Nguyen and others.
- COOL - a generic reasoner for coalgebraic logics which not only
handles basic logics like Multimodal K (aka ALC) or Probabilistic
Modal Logic or Coalition Logic but also any possible combination of them.
- CTL tableau provers - One pass tree-tableau and graph-tableau multipass provers for computational tree logic. By group of Rajeev Gore.
- DLP - An experimental tableaux-based inference system by Peter Patel-Schneider for a range of description logics.
- ELVis - A suite of sequent calculus based automated theorem provers and GUI Kripke model editors for epistemic logics including PAL and DEL by Shoshin Nomura.
- FaCT++ - A tableaux-based description logic OWL reasoner by Ian Horrocks and Dmitry Tsarkov. Successor of FaCT.
- FAME - An automated tool for semantic forgetting in expressive description logics.
- Gen2Sat - Sat-based decision procedure and web-based tool for analytic pure sequent calculi, implemented by Yoni Zohar. It can be used for modal logic KDalt1 (in which the accessibility relation is a function).
- GOAL - A graphical interactive tool for defining and manipulating Büchi automata and propositional and quantified propositional temporal logic formulae.
- Gost - A Lisp implementation of a tableau algorithm for GF1-, a sublogic of the "First Guarded Fragment".
- KSP - A resolution-based prover for propositional multimodal K.
- KtSeqC - A theorem prover for the minimal tense logic Kt.
- LCKS5 tableau prover - Graph-based tableau prover for propositional logic of common knowledge with S5 agent modalities. By group of Rajeev Gore.
- LETHE - Forgetting and uniform interpolation tool for description logic based ontologies.
- LoTREC - A generic tableau theorem prover for modal logic, which is suitable for creating, testing and analysing tableau method implementations.
- MDK-verifier - Checker able to tell for the modal logic K if formula is true in a given Kripke model or to tell why it is not the case. Kripke models are produced in png. Written in C++ by Valentin Montmirail.
- MetTeL - A tableau prover generator. Implemented by Dmitry Tishkovsky.
- mleanCop - A compact automated theorem prover for modal first-order logic based on the clausal connection calculus for modal logic.
- mleanTap - A Prolog implementation of a sound and complete theorem prover for some first-order modal logics, based on free-variable semantic tableaux extended by an additional prefix unification to ensure the particular restrictions in modal logics.
- 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
- NESCOND - A theorem prover for Conditional Logics based on nested sequent calculi for normal conditional logics. By Nicola
Olivetti and Gian Luca Pozzato.
- pdl-tableau - A prototypical implementation of the tableau calculus for PDL-formulae not involving nested stars. Implemented by Renate Schmidt.
Web interface
- PDL tableau provers, and with converse - Graph-based and tree-based decision procedures for propositional dynamic logic, and with converse. By group of Rajeev Gore.
- PLTL provers - Three provers for propositional linear temporal logic: tableau prover based on Schwendimann's method, graph-based prover based on Wolper's method and prover creating the set of all CPL-consistent subsets of the Fischer-Ladner closure. By group of Rajeev Gore.
- 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.
- Sibyl - A theorem prover for multi-modal hybrid logic with binders, the converse
and global modalities, transitivity assertions and relation hierarchies,
developed at University of Roma Tre.
- SMCDEL - A symbolic model checker for Dynamic Epistemic Logic.
Developed by Malvin Gattinger at the University of Amsterdam.
Web interface with examples
- 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.
- SPASS-tab - A
tableau-resolution prover built as an extension of the first-order
resolution theorm prover SPASS that simulates semantic tableau provers
for extended modal 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.
- TATL - A tableau-based decision procedure for the alternating-time temporal logic (ATL) by Amelie David.
- 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.
- 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.
- TSPASS - A fair theorem prover for the monodic
fragment of first-order linear-time temporal logic over expanding
domains based on the temporal resolution calculus, developed by Michel
Ludwig.
- 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 temporal logics.
Verifiers
- MDK-verifier - Checker able to tell for the modal logic K if formula is true in a given Kripke model or to tell why it is not the case. Kripke models are produced in png. Written in C++ by Valentin Montmirail.
Translators
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.
Other tools
- Hintikka's world - Pedagogical tool for showing how artificial agents can reason about higher-order knowledge (an agent knows that another agent knows that...). The system includes a variety of AI examples including Muddy children and Russian cards. The system allows to implement user's own examples via the description of a Kripke model or via its generation by the generic tableau method prover MetTeL2.
- Parser InToHyLo - Open-source parser for modal logic formulae. Containing already the shift and reduce algorithm plus all the classes to manipulate the formulae in the InToHyLo format. Written in C++ by Valentin Montmirail.
Generators of formulae
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.
Also of interest: Benchmark formulae for intuitionistic propositional logic.
Related links