Prover9 Manual and Examples

Please use the version of the manual and examples that matches your version of LADR.

2009-11A (November 2009): Manual Examples (current)
2009-02A (February): Manual Examples
2008-11A (November): Manual Examples
2008-09A (September): Manual Examples
2008-06A (June): Manual Examples
2008-05A (May): Manual Examples
2008-04A (April): Manual Examples
Dec-2007: Manual Examples
Oct-2007: Manual Examples
Aug-2007: Manual Examples
June-2007: Manual Examples
May-2007: Manual Examples
April-2007: Manual Examples
March-2007: Manual Examples

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.
August-2006A: Manual Examples
September-2006: Manual Examples
November-2006: Manual Examples
January-2007: Manual Examples

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).

June-2006C: Manual Examples

Nothing is available for versions before June-2006C.


Download the Manual and Supporting Files (HTML)

(These are essentially the same as the online versions above.)