Automated theorem proving
From Academic Kids

Automated theorem proving (currently the most important subfield of automated reasoning) is the proving of mathematical theorems by a computer program. Depending on the underlying logic, the problem of deciding the validity of a theorem varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but NPcomplete, and hence only exponential time algorithms are believed to exist. For firstorder logic it is recursively enumerable, i.e., given unbounded resources, any true theorem can eventually be proven, but invalid theorems cannot always be recognized. Despite these theoretical limits, practical theorem provers can solve many hard problems in these logics.
A simpler, but related problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.
Interactive theorem provers require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have by now proven a number of interesting and hard theorems, including some that have eluded human mathematicians for a long time. However, these successes are sporadic, and work on hard problems usually requires a proficient user.
Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking, which is equivalent to bruteforce enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force). There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machineaided proof of the four color theorem, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called nonsurveyable proofs). Another example would be the proof that the game Connect Four is a win for the first player.
Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny. In the latest processors from AMD, Intel, and others, automated theorem proving has been used to verify that the divide and other operations are correct.
Contents 
Popular techniques
 Firstorder resolution
 Term rewriting
 Model checking
 Mathematical induction
 Binary decision diagrams
 Unification
 Higherorder unification
Available implementations
 ACL2
 Carine
 Coq
 CVC Lite
 E
 Isabelle
 Gandalf
 HOL
 LCF
 MetaPRL
 Mizar
 NuPRL
 Otter
 Paradox
 PhoX
 PVS
 Simplify
 SPASS
 Twelf
 Vampire
 Waldmeister
You can find information on some of these theorem provers and others at http://www.tptp.org/CASC/J2/SystemDescriptions.html. The TPTP library of test problems, suitable for testing firstorder theorem provers, is available at http://www.tptp.org, and solutions from many of these provers for TPTP problems are in the TSTP solution library, available at http://www.tptp.org/TSTP .
Important people
 Leo Bachmair
 Robert Stephen Boyer
 Bill McCune
 Robert Constable
 Martin Davis
 Harald Ganzinger
 Michael Genesereth
 Michael J. C. Gordon
 Donald W. Loveland
 Sergei Maslov
 J Strother Moore
 Robert Nieuwenhuis
 Tobias Nipkow
 Ross Overbeek
 Lawrence C. Paulson
 David A. Plaisted
 John Rushby
 Alan Robinson
 Natarajan Shankar
 Robert Veroff
 Andrei Voronkov
 Larry Wos
References (books)
 Symbolic Logic and Mechanical Theorem Proving. ChinLiang Chang and Richard CharTung Lee. Academic Press (1973)
 Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. Donald W. Loveland. NorthHolland Publishing (1978)
 Logic for Computer Science: Foundations of Automatic Theorem Proving. Jean H. Gallier. Harper & Row Publishers (1986) Download (http://www.cis.upenn.edu/~jean/gbooks/logic.html)
 Principles of Automated Theorem Proving. David A. Duffy. John Wiley & sons (1991)
 Automated Reasoning: Introduction and Applications (2nd edition). Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. McGrawHill (1992)
 Handbook of Automated Reasoning Volume I & II. Alan Robinson and Andrei Voronkov (eds.) Elsevier and MIT Press (2001)pl:Automatyczne dowodzenie twierdzeńde:Computerbeweis