Integrating Specialized Procedures in Proof Systems

Abstract

Ever since its early days, one of the goals in AI has been the development of general systems that can utilize the benefits of specialized reasoners. Recently, research on hybrid reasoning systems has led to the following problem: Can a formalism be developed that allows specialized procedures to be flexibly integrated into a general purpose reasoner? In this thesis, we present ${\cal C}$-FOL--a formalism for integrating specialized procedures into proof systems. Existing approaches to solving this problem lack two important properties: flexibility, and generality. This thesis is motivated by the intuition that in order to flexibly integrate specialized procedures into a proof system, specialized procedures should be described to it, instead of being built-in. We describe the extensions to the syntax, semantics, and inference machinery of a proof system so as to enable both the description of specialized procedures, as well as their use. We show how this allows C-FOL to (i) extend the existing integration techniques such as those based on attachments, and (ii) achieve the generality such as that envisioned in some types of theory resolution, e.g. partial-narrow theory resolution. We study two famous AI systems that are viewed as instances of theory resolution, and show that not only can C-FOL perform the same types of reasoning, but that it provides a way to, in general, implement some types of theory resolution. We also present soundness and completeness results pertaining to C-FOL, and some other results pertaining to control issues that arise in the context of hybrid reasoning. We conclude by putting our work in perspective, against the backdrop of AI research in the gray area of between deduction and computation.