Software

The software sources on this site are all freely available for download and private use. Please note, however, that copyright subsists in all of these materials and vests in the Australian National University. Permission is not given to make use of any code from this site in commercial products or for any commercial purpose without prior express permission from the Australian National University. The Australian National University makes no representation as to the suitability of this software for any purpose. Nor does it accept any responsibility for any loss, damage or ridicule resulting from the installation or use of this software.

That's all for warnings. You may now download the programs and install them. Some of them may even work.

  • KRIPKE: a prehistoric theorem prover for relevant logic, written by Paul Thistlewaite and extensively commented by Gustav Meglicki.

  • MaGIC: the Matrix Generator for Implication Connectives. You need this tool if you work with non-classical propositional logics, especially of the substructural sort. The sources now include amendments by Gert-Jan Lokhorst so that they should compile under MS-Windows as well as under Solaris, MacOS-X, etc. See his MaGIC page for more information.

  • FINDER: Finite domain enumerator. This is a finite domain CSP solver, rather limited in what it can do. Don't expect it to deal effectively with anything numerical, though it can knock off small problems reasonably quickly. The nice feature (say I) is the input language which is first order logic thinly disguised. Earlier versions of this came with some documentation. This one comes with the injunction to use the Force (read the source). Also read the README that comes with it.

  • Minlog: a no-frills theorem prover for propositional minimal logic and intuitionist logic. Works OK as long as formulae only contain a small number of variables. Proofs appear in a weird Fitch style without annotation. Popular, for some reason.

  • Otter: the well known prover by Bill McCune. Version 3.2 is no longer the latest, so if you really want Otter it's better to get it from Bill's web site at Argonne National Lab. Better still, get Prover9.

  • Randomnet: a rather specific-purpose tool. Generates random descriptions of power distribution networks as part of the PSR (Power Supply Restoration) benchmark for AI planning. See Sylvie Thiébaux's home page for more information.

  • SOS: Son Of SCOTT. This is a semantically-guided first order theorem prover built around Otter and using FINDER to generate (approximate) models of clause sets for guidance purposes. Very experimental: comes with nothing but the sources. For a description of the online help facility, type "man grep".

  • SOS again: Another version of the above with better memory management and a few bugs fixed. Posted in 2006. 

    • Dr J K Slaney                      Phone (Aus.):  (026) 125 8607
Automated Reasoning Project        Phone (Int.): +61 26 125 8607
Australian National University     Fax (Aus.):    (026) 125 8651
Canberra, ACT, 0200, AUSTRALIA     Fax (Int.):   +61 26 125 8651
    John.Slaney@anu.edu.au