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.
a prehistoric theorem prover for relevant logic, written by Paul
Thistlewaite and extensively commented by Gustav Meglicki.
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 home page for more information.
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.
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.
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.
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".
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