Prover9 is an Automated theorem proving automated theorem prover for First order logic 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 GNU General Public License 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 ... of list. External links http www.cs.unm.edu mccune prover9Prover9 home page http forums.prover9.org Prover9 Mace4 LADR forums http dwheeler.com formal methods Formal methods square root of 2 example ... more details
Infobox scientist name William McCune image image width 200px caption William McCune residence USA nationality American field Computer Technology work institution University of New Mexico known for Otter , Mace automated reasoning system Mace , Prover9 , Robbins conjecture William McCune is an United States American computer scientist working in the fields of Automated reasoning , Algebra , Logic , and Formal Methods . He is best known for the development of the Otter theorem prover , Prover9 , and Mace automated reasoning system Mace automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP theorem prover. External links http www.cs.unm.edu mccune Home page Persondata Metadata see Wikipedia Persondata . NAME Maccune, William ALTERNATIVE NAMES SHORT DESCRIPTION DATE OF BIRTH PLACE OF BIRTH DATE OF DEATH PLACE OF DEATH DEFAULTSORT Maccune, William Category Living people US scientist stub ... more details
Otter is an Automated theorem proving 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. Otter is an acronym for Organized Techniques for Theorem proving and Effective Research . Otter has been very stable for a number of years but is no longer actively developed. As of November 2008, the last changelog entry was dated 14 September 2004. A successor to Otter is Prover9 . The software is in the public domain . The University of Chicago has declined to assert its copyrights in this software, and it may be used, modified, and redistributed with or without modifications by the public. According to Wos and Pieper, OTTER is written in approximately 28,000 lines of C programming language. References cite journal first William last McCune coauthors Larry Wos title Otter The CADE 13 Competition Incarnations journal Journal of Automated Reasoning volume 18 issue 2 pages 211 220 year 1997 doi 10.1023 A 1005843632307 Kalman, John Arnold. cite Automated Reasoning with OTTER cite . ISBN 1 58949 004 5 External links http www.cs.unm.edu mccune otter Otter home page http www.cs.unm.edu mccune prover9 Prover9 home page logic stub Category Free theorem provers Category Public domain software ... more details
has since been replaced by Prover9 theorem prover Prover9 , which is paired with Mace4 . SETHEO ... Version Last update Author Prover9 Mace4 ? No Yes Yes v05 11 2009 William McCune Argonne National ... more details
Encyclopedia
top
