Catalogue of Artificial Intelligence Techniques
Categories: Inference and Reasoning , Theorem Proving
Author(s): Alan Smaill
While automated Theorem Proving aims to show automatically that a statement is derivable in a formal system, a proof editor is designed so that the user can construct derivations interactively, with the implementation taking care to ensure that the resultant derivation is correct. Proof editors are employed because theorem proving in most logics is difficult or impossible to automate fully. In practice, systems not only allow the user to invoke rules of inference individually but also allow for some automation, for example by incorporating decision procedures for some classes of problems, or by allowing chains of inference applications to be applied automatically. A procedure which applies an appropriate chain of inference rules to a given problem is often called a tactic. A proof editor, apart from maintaining the logical correctness of proofs, should ideally aid in operations such as instantiation of variables, recall of earlier proof states, recording of dependencies between proofs, and manipulation of partially specified proofs. The user may be aided by indication of possible `next steps' in the construction. Most proof editors are tailored to a particular logic, but there has recently been interest in proof editors that can be customised over a large range of logics.
- Huet, G. and Plotkin, G.D., Logical Frameworks
, Cambridge University Press, Cambridge, England, 1991.