Software

  1. ModLeanTap: a theorem prover for modal logic K based upon LeanTap.
  2. The Tableau Work Bench: a generic tableau engine for building propositional theorem provers for nonclassical logics.
  3. dRA: Isabelle/HOL theories formalising the display calculus for relation algebras.
  4. CardS4: Modal Theorem Proving on Java Smart Cards.
  5. CardKt: Automated Multi-modal Deduction on Java Smart Cards.
  6. The world's first theorem prover on a smart card.
  7. A theorem prover for propositional tense logic Kt.
  8. A satisfiability checker for description logic ALC with inverse roles (ALCI) also known as propositional mutimodal Kt written in Ocaml.
  9. A theorem prover for propositional bi-intuitionistic logic written by Linda postniece.
  10. Benchmark formulae for testing provers for ALC with inverse roles (ALCI).
  11. Three satisfiability checkers for propositional linear temporal logic PLTL.
  12. Three satisfiability/validity checkers for Computation Tree Logic (CTL).
  13. Benchmark formulae for testing provers for Computation Tree Logic (CTL).
  14. Two satisfiability checkers for propositional dynamic logic PDL.
  15. Benchmark formulae for testing provers for Propositional Dynamic Logic (PDL).
  16. A satisfiability checker for propositional dynamic logic with converse (CPDL).
  17. A satisfiability checker for propositional logic of common knowledge with S5 agent modalities (LCKS5).
  18. A satisfiability, falsifiability and validity checker for propositional bi-intuitionistic tense logics, plus randomly generated formulae of intuitionistic logic.
  19. An optimised satisfiability, falsifiability and validity checker for propositional bi-intuitionistic tense logic
  20. BDDTab: A tableau theorem prover for modal logics K, S4 and description logic ALC which uses binary decision diagrams (BDDs) as an underlying data-structure. Benchmark formulae and translators from OWL syntax into our syntax are also provided here.
  21. 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 co-authors wrote a separate program to refine the output produced by procmine as outlined in the paper.
  22. 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: +61-2-6125 8603 
Logic and Computation Group    Fax: +61-2-6125 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