An Integration of Resolution and Natural Deduction Theorem Proving

Dale Miller, Amy Felty

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 expansion 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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.