LADR v2009-11A

LADR (Library for Automated Deduction Research) includes Prover9, Mace4, and several related programs. Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

Accessing the software

To load the module:

$ module load apps/ladr/v2009-11a

An example command to include in your job script:

prover9 < <prover_input_file>

where <prover_input_file> is the input file to direct into stdin for prover9.

The modulefile also sets the environment variables:

  • MACE4_EXAMPLES to refer to a directory containing MACE4 examples.
  • PROVER9_EXAMPLES to refer to a directory containing PROVER9 examples.

Accessing Previous Versions

Wherever possible, previous versions of this application will be retained for continuity, especially for research projects that require a consistent version of the software throughout the project. Such versions, however, may be unsupported by IT Services or the applications vendor, and may be withdrawn at short or no notice if they can no longer run on the cluster - for example, essential operating system upgrades may be incompatible with old versions.

At present there are no previous versions of this application on the BlueBEAR service.

Known Problems & Limitations


Other Information

The Support Level for this application is An.

Visit the Prover9 and Mace4 website for more information regarding this application.

Last modified: 30 November 2017