An Integration of Resolution and Natural Deduction Theorem Proving

We present a high-level approach to the integration of such different theorem proving technologies as resolution and natural deduction. This system represents natural deduction proofs as X-terms and resolution refutations as the types of such X-terms. These type structures, called ezpansion trees, are essentially formulas in which substitution terms are attached to quantifiers. As such, this approach to proofs and their types extends the formulas-as-type notion found in proof theory. The LCF notion of tactics and tacticals can also be extended to incorporate proofs as typed X-terms. Such extended tacticals can be used to program different interactive and automatic natural deduction theorem provers. Explicit representation of proofs as typed values within a programming language provides several capabilities not generally found in other theorem proving systems. For example, it is possible to write a tactic which can take the type specified by a resolution refutation and automatically construct a complete natural deduction proof. Such a capability can be of use in the development of user oriented explanation facilities.