Prover9
Encyclopedia
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
.
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 was under active development, with new releases every month or every other month, until 2009. Prover9 is free software
/open source software; it is released under GPL
version 2 or later.
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.
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 b/c 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.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
for First-order and equational logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
developed by William McCune
William McCune
William McCune was an American computer scientist working in the fields of Automated reasoning, Algebra, Logic, and Formal Methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP...
. Prover9 is the successor of the Otter theorem prover
Otter theorem prover
Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois. Otter was the first widely distributed, high-performance theorem prover for first-order logic, and it pioneered a number of important implementation techniques...
.
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 was under active development, with new releases every month or every other month, until 2009. Prover9 is free software
Free software
Free software, software libre or libre software is software that can be used, studied, and modified without restriction, and which can be copied and redistributed in modified or unmodified form either without restriction, or with restrictions that only ensure that further recipients can also do...
/open source software; it is released under GPL
GNU General Public License
The GNU General Public License is the most widely used free software license, originally written by Richard Stallman for the GNU Project....
version 2 or later.
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*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 b/c 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.