Prover9 Manual and Examples
Please use the version of the manual and examples
that matches your version of LADR.
Nothing is available for versions before June-2006C.
A major change in the LADR/Prover9/Mace4 input language occurred
in July 2006.
The type distinction between "clauses" and "formulas" disappeared; "formulas"
can now have free variables; and "clauses" are now a subset of "formulas".
All lists of formulas (clausal and non-clausal) start with
formulas(listname).
A major change was made in Prover9's given-clause selection procedure.
The old method is no longer available, and most searches cannot
be exactly reproduced.
Download the Whole Prover9 Manual and Supporting Files (HTML)