Integrating Specialized Procedures in Proof Systems

We present the outline of a simple but powerful scheme for describing procedures that can be used by an automatic theorem prover. Our approach is to describe specialized procedures to a theorem prover by adding procedure description axioms to its set of facts, instead of building in these procedures by using attachments. Our work can be viewed as an extension of the hybrid reasoning techniques based on attachments (Myers91). In this abstract we briefly describe our approach and state some of its advantages. In (Sikka94), we present this work in detail and formally show how the full expressibility of attachment-like approaches can be achieved in a simple logic-theoretic way. The work described here is part of the author' s Ph.D. thesis research in collaboration with Prof. Michael Genesereth.