The following programs have been developed in the ARG and are available from this site. Please note that most of them represent research work in progress, so no guarantee is made as to their suitability for any purpose. Nor do the authors, the Computer Sciences Laboratory or the Australian National University give any undertaking to support or maintain any of this software. 

SCOTT (Semantically Constrained Otter) 
 

FINDER (Finite Domain Enumerator) 
 

MaGIC (Matrix Generator for Implication Connectives) 
 

BWSTATES (Generate States of Blocks World) 
 

MINLOG (A Theorem Prover for Minimal and Intuitionistic Logic) 
 

KRIPKE (A Theorem Prover for the Relevant Logic LR). 
 

ModLeanTAP (A lean tableaux based prover for modal logics written in Sicstus Prolog) 
 

CardTAP (A very lean tableaux based prover designed for small systems like smart cards written in Java) 
 

KtSeqC (A sequent system prover for the modal tense logic Kt written in C)
 

CardKt (A lean modal theorem prover for smart cards combining ideas from CardTAP and KtSeqC)
 

CardS4 (A lean theorem prover for modal logic S4 that runs on Java cards)
 

PicLay (An Evolutionary Approach to Support Web-Page Design)
 

Esc (Evolutionary Search for Combinators)