Prover9

Description

Prover9 is the successor of the Otter theorem prover also developed by William McCune.[1]: 1  Prover9 is noted for producing relatively readable proofs and having a powerful hints strategy.[1]: 11 

Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously from the same input,[2] 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 ("Library for Automated Deduction Research") 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 was under active development, with new releases every month or every other month, until 2009. Prover9 is free software, and therefore, 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:[3]

formulas(assumptions).
  1*x = x.                            % identity
  x*y = y*x.                          % commutativity
  x*(y*z) = (x*y)*z.                  % associativity
  ( x*y = x*z ) -> y = z.             % cancellation (0 is not allowed, so x!=0).
  %
  % Now let's define divides(x,y): x divides y.
  %   Example: divides(2,6) is true because 2*3=6.
  %
  divides(x,y) <-> (exists z x*z = y).
  divides(2,x*x) -> divides(2,x).     % If 2 divides x*x, it divides x.
  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.

References
  1. Phillips, J. D.; Stanovsky, David. "Automated Theorem Proving in Loop Theory" (PDF). Charles University. Archived (PDF) from the original on 28 March 2018. Retrieved 15 November 2018.
  2. Berghammer, Rudolf; Struth, Georg (21 June 2010). "On Automated Program Construction and Verification" (PDF). In Bolduc, Claude; Desharnais, Jules; Ktari, Bechir (eds.). Mathematics of Program Construction, Proceedings. 10th International Conference, MPC 2010. Quebec City. doi:10.1007/978-3-642-13321-3. ISBN 978-3-642-13320-6. S2CID 6962311. Archived from the original (PDF) on 19 November 2018. Retrieved 19 November 2018.
  3. Wheeler, David A. "sqrt2.in". David A. Wheeler’s Personal Home Page. Retrieved 14 March 2016.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.