Prover9

Prover9

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

* [http://www.cs.unm.edu/~mccune/prover9/ Prover9 home page]
* [http://dwheeler.com/formal_methods/ Formal methods (square root of 2 example)]


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • 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… …   Wikipedia

  • Ontological argument — The ontological argument for the existence of God (or simply ontological argument) is an a priori proof for the existence of God. The ontological argument was first proposed by the eleventh century monk Anselm of Canterbury, who defined God as… …   Wikipedia

  • William McCune — Infobox Scientist name = William McCune image width= 200px caption = William McCune residence = USA nationality = American field = Computer Technology work institution = University of New Mexico known for = Otter, Mace, Prover9, Robbins… …   Wikipedia

  • Demostración automática de teoremas — Saltar a navegación, búsqueda Para otros usos de este término, véase Demostración. La demostración automática de teoremas (de siglas ATP, por el término en inglés …   Wikipedia Español

  • Онтологический аргумент — Онтологический аргумент  это одна из категорий аргументов, относящихся к вопросу существования Бога, появившаяся в Христианской Теологии. Не существует точных критериев для классификации онтологических аргументов, но аргументы типично… …   Википедия

  • Resolution (logic) — In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem proving technique for sentences in propositional logic and first order logic. In other words, iteratively applying the… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”