Added to Favorites

Popular Searches

Definitions

Nearby Words

Prover9 is an automated theorem prover for First-order and equational logic developed by William McCune. Prover9 is the successor of the Otter theorem prover.## Examples

### Socrates

### Square Root of 2 is irrational

## External links

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.

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.

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.

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Saturday May 31, 2008 at 07:00:47 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Saturday May 31, 2008 at 07:00:47 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2015 Dictionary.com, LLC. All rights reserved.