Software

ModLeanTap: a theorem prover for modal logic K based upon LeanTap.

The Tableau Work Bench: a generic tableau engine for building
propositional theorem provers for nonclassical logics.

dRA: Isabelle/HOL theories formalising the display calculus for
relation algebras.

CardS4: Modal Theorem Proving on Java Smart Cards.

CardKt: Automated Multimodal Deduction on Java Smart Cards.

The world's first theorem prover on a smart card.

A theorem prover for propositional tense logic Kt.

A satisfiability checker for description logic ALC with inverse roles (ALCI) also known as propositional mutimodal Kt written in Ocaml.

A theorem prover for propositional biintuitionistic logic written by Linda postniece.

Benchmark formulae for testing provers for ALC with inverse roles (ALCI).

Three satisfiability checkers for propositional linear temporal logic PLTL.

Three satisfiability/validity checkers for Computation Tree Logic (CTL).

Benchmark formulae for testing provers for Computation Tree Logic (CTL).

Two satisfiability checkers for propositional dynamic logic PDL.

Benchmark formulae for testing provers for Propositional Dynamic Logic (PDL).

A satisfiability checker for propositional dynamic logic with converse (CPDL).

A satisfiability checker for propositional logic of common knowledge with S5 agent modalities (LCKS5).

A satisfiability, falsifiability and validity checker for propositional biintuitionistic tense logics, plus randomly generated formulae of intuitionistic logic.

An optimised satisfiability, falsifiability and validity checker for propositional biintuitionistic tense logic
 BDDTab:
A tableau
theorem prover for modal logics K, S4 and description logic ALC
which uses binary decision diagrams (BDDs) as an underlying
datastructure. Benchmark formulae and translators from OWL syntax
into our syntax are also provided here.

A tool to synthesise business process templates from logical specifications.
An OCaml program that reads a file of domain knowledge in a specific format and a set of constraints
in propositional linear temporal logic (PLTL) and then outputs a graphical representation of the business process template corresponding to a
linear temporal logic model of the satisfiability problem associated with these inputs. We also provide tools to pinpoint the inconsistency if the
problem associated with the inputs is unsatisfiable. See also Awad et al on my papers listing. The output of procmine is not the final output mentioned in
this paper as our coauthors wrote a separate program to refine the output produced by procmine as outlined in the paper.
 IntHistGC: A
theorem prover for propositional intuitionistic logic
which uses a sequent calculus with histories and global caching.
Some benchmark generators are also provided here.
Prof. Rajeev P. Goré Tel: +6126125 8603
Logic and Computation Group Fax: +6126125 8651
Research School of Computer Science Email: Rajeev.Gore at anu.edu.au
Australian National University
Canberra, ACT, 2601, AUSTRALIA
ANU CRICOS Provider Number  00120C
Rajeev.Gore at anu.edu.au