Automated Deduction by Theory Resolution

Abstract

Theory resolution constitutes a set of complete procedures for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory. This can greatly reduce the length of proofs and the size of the search space. Theory resolution efl'ects a beneficial division of Iabor, improving the performance of the theorem prover and increasing the applicability of the specialized reasoning procedures. Applications include the building in of both mathemat· ical and special decision. procedures, e.g., for the taxonomic information furnished by a knowledge representation system . Theory resolution is a generalization of numerous previously known resolution refinements. lts power is demonstrated by comparing solutions of "Schubert's Steamroller" challenge problern with and without building in axioms through theory resolution.