Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously from the same input, with Prover9 attempting to find a proof, while Mace4 attempts to find a (disproving) counter-example. Prover9, Mace4, and many other tools are built on an underlying library named LADR to simplify implementation. Resulting proofs can be double-checked by Ivy, a proof-checking tool that has been separately verified using ACL2.

In July 2006 the LADR/Prover9/Mace4 input language made a major change (which also differentiates it from Otter). The key distinction between "clauses" and "formulas" completely disappeared; "formulas" can now have free variables; and "clauses" are now a subset of "formulas". Prover9/Mace4 also supports a "goal" type of formula, which is automatically negated for proof. Prover9 attempts to automatically generate a proof by default; in contrast, Otter's automatic mode must be explicitly set.

Prover9 is under active development, with new releases every month or every other month. Prover9 is free software/open source software; it is released under GPL version 2 or later.

Examples

Socrates

The traditional "all men are mortal", "Socrates is a man", prove "Socrates is mortal" can be expressed this way in Prover9:

formulas(assumptions).

  man(x) -> mortal(x).   % open formula with free variable x

  man(socrates).

end_of_list.

formulas(goals).

  mortal(socrates).

end_of_list.

This will be automatically converted into clausal form (which Prover9 also accepts):

formulas(sos).

  -man(x) | mortal(x).

  man(socrates).

  -mortal(socrates).

end_of_list.

Square Root of 2 is irrational

A proof that the square root of 2 is irrational can be expressed this way:

formulas(assumptions).

  1*x = x.                            % identity

  x*1 = x.

  x*(y*z) = (x*y)*z.                  % associativity

  x*y = y*x.                          % commutativity

  (x*y = x*z ) -> y = z.              % cancellation (0 is not allowed, so x!=0).

  %

  % Now let's define divides(x,y): x divides y.  divides(2,6) is true b/c 2*3=6.

  %

  divides(x,y) <-> (exists z x*z = y).

  divides(2,x*y) ->

    (divides(2,x) | divides(2,y)).    % If 2 divides x*y, it divides x or y.

  a*a = (2*(b*b)).                    % a/b = sqrt(2), so a^2 = 2 * b^2.

  (x != 1) ->  -(divides(x,a) &

              divides(x,b)).          % a/b is in lowest terms

  2 != 1.                             % Original author almost forgot this.

end_of_list.

External links

• Prover9 home page
• Formal methods (square root of 2 example)