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.
   

Dr. 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 Information Sciences and Engineering 
Australian National University 
Canberra, ACT, 0200, AUSTRALIA     
ANU CRICOS Provider Number - 00120C