Catalogue of Artificial Intelligence Techniques
Aliases: Automatic Theorem Proving, Computational Logic, Mechanical Theorem Proving
Keywords: Natural Deduction
Categories: Inference and Reasoning , Problem Solving , Theorem Proving
Author(s): Fausto Giunchiglia
The goal of theorem proving is to use mechanical methods for finding proofs of theorems to perform automated reasoning. The implementation language is usually First-order Logic, or some other sound and complete formalism. The problem can be stated as follows: given a set of hypotheses (axioms and/or theorems), a set of rules (called the rules of inference) which allow new facts to be derived from old, a given formula (the goal) should be derived in finitely many applications of the rules of inference. Besides mathematical reasoning, which is the obvious application, many problems can be transformed into theorem proving problems: question-answering systems, program-synthesis, program verification, state transformation problems and so on. Some theorem proving techniques are based on Herbrand's theorem (e.g., Resolution, Connection Calculus) but some attempts have been made using natural deduction-based, and induction-based systems (see Recursion Analysis). The reference provides a very good collection of many of the early attempts (up to 1970) in theorem proving.
- Siekmann, J. and Wrightson, G., eds., Automation of Reasoning
, Springer-Verlag, Berlin, 1983 (Published in 2 volumes