Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Theorem Proving

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.



Add Comment

No comments.