Software

  1. The Tableau Work Bench: a generic tableau engine for building propositional theorem provers for nonclassical logics.
  2. dRA: Isabelle/HOL theories formalising the display calculus for relation algebras.
  3. CardS4: Modal Theorem Proving on Java Smart Cards.
  4. CardKt: Automated Multi-modal Deduction on Java Smart Cards.
  5. The world's first theorem prover on a smart card.
  6. A theorem prover for propositional tense logic Kt.
  7. A satisfiability checker for description logic ALC with inverse roles (ALCI) also known as propositional mutimodal Kt written in Ocaml.
  8. A theorem prover for propositional bi-intuitionistic logic written by Linda postniece.
  9. Benchmark formulae for testing provers for ALC with inverse roles (ALCI).
  10. Two satisfiability checkers for propositional linear temporal logic PLTL.
  11. Two satisfiability checkers for Computation Tree Logic (CTL).
  12. Benchmark formulae for testing provers for Computation Tree Logic (CTL).
  13. Two satisfiability checkers for propositional dynamic logic PDL.
  14. Benchmark formulae for testing provers for Propositional Dynamic Logic (PDL).
  15. A satisfiability checker for propositional dynamic logic with converse (CPDL).
  16. A satisfiability checker for propositional logic of common knowledge with S5 agent modalities (LCKS5).
  17. A satisfiability, falsifiability and validity checker for propositional bi-intuitionistic tense logics, plus randomly generated formulae of intuitionistic logic.
Prof. Rajeev P. Goré         Tel: +61-2-6125 8603 
Automated Reasoning Group    Fax: +61-2-6125 8651 
Computer Sciences Laboratory Email: Rajeev.Gore at anu.edu.au
Research School of Computer Science 
Australian National University 
Canberra, ACT, 0200, AUSTRALIA     
ANU CRICOS Provider Number - 00120C
Rajeev.Gore at anu.edu.au