Automated theorem proving

Gries95] Gries, D., and F. B. Schneider, Eds. 1995. First-Order Logic and Automated Theorem Proving, 2d ed. New York Springer-Verlag. 

Godel s incompleteness theorem (proved by Austrian-born American mathematician Kurt Godel) shows that it may not be possible to automatically prove an arbitrary theorem in systems as complex as the natural numbers. For simpler systems, such as group theory, automated theorem proving works if the user s computer can generate all reverse trees or a suitable subset of trees that can yield a... 

Note that deductive inference is always sound. Typical rules of deductive inference are modusponens, universal instantiation, resolution, mathematical induction, and so on. The branch of artificial intelligence research that is bent on automating deductive inference is called automated theorem proving. 

The notes offered here do not distinguish between different kinds of formal method. There is a world of difference between, say, formal specification and automated theorem-proving, though both fall under the general rubric of formal methods. In addition, formal methods are applied to different components of a system which introduces important variations in their purpose and use. Again, these are not explored here. 

Thus, my conclusion is that to describe safety case arguments, we need a formalism that includes quantification, uninterpieted predicates and constants, set theory, and arithmetic - but the theorem proving needs pushbutton automation only for the unquantified case. These capabilities are (a subset of) the capabihties of formahsms built on, or employing, SMT solvers (i.e., solvers for the problem of Satisfiabihty Modulo Theories) (Rushby 2006). Modem SMT solvers are very effective, often able to solve problems with hundreds of variables and thousands of constraints in seconds. They are the subject of an aimual competition, and this has driven very rapid improvement in both their performance and the range of theories over which they operate. 

Theorem Provers. Most theorems in mathematics can be expressed in first-order predicate calculus. For any particular area, such as synthetic geometry or group theory, all provable theorems can be derived from a set of axioms. Mathematicians have written programs to automatically prove theorems since the 1950 s. These theorem provers either start with the axioms and apply an inference technique, or start with the theorem and work backward to see how it can be derived from axioms. Resolution, developed in Prolog, is a well-known automated technique that can be used to prove theorems, but there are many others. For Resolution, the user starts with the theorem, converts it to a normal form, and then mechanically builds reverse decision trees to prove the theorem. If a reverse decision tree whose leaf nodes are all axioms is found, then a proof of the theorem has been discovered. 

---