Prover9

Prover9 is an automated theorem prover for first-order logic with equality. It is designed to be a practical, portable, and freely available successor to Otter, developed by William McCune. Prover9 focuses on efficient search for formal proofs and is intended for use in research and education in automated reasoning.

Prover9 is written in C and implements a given-clause saturation algorithm, combining resolution with paramodulation to handle equality. It supports rewrite rules (demodulation) to orient equations for faster inference, and it offers an optional hint mechanism to guide search toward relevant parts of the search space. It exposes various parameters for inference control and proof search tuning.

Prover9 reads problems in a human-readable first-order logic syntax similar to Otter; problems can be submitted via files or standard input. It can output proofs and a trace of the inference sequence, and can report whether a conjecture is a consequence of the given axioms.

The tool is used in theoretical computer science, formal methods, and education, to verify conjectures and experiment with automated reasoning techniques. It is often used with Mace4, a related finite-model finder, to obtain countermodels or to study models of the given theory.

Prover9 and Mace4 are freely available from the author’s website and run on Unix-like systems and Windows.