A category theory approach to completion-based theorem proving strategies (Abstract)

In this paper we apply category theory to formalize the basic concepts of automated theorem proving. A theorem proving strategy is given by a set of inference rules and a search plan. For the inference rules, we propose a new characterization of inference rules as natural transformations. Traditionally, inference rules are presented either as functions or as rules to transform sets of sentences. Neither description is completely satisfactory, especially if contraction inference rules, i.e. rules that delete sentences, are involved. Our view of inference rules as natural transformation couples the advantages of the two traditional approaches: it applies to both expansion and contraction rules, while still saving the functional nature of inference rules. The search plan selects at each stage of a derivation the inference rule and the premises for the next step. In most theorem proving strategies the search plans are described informally or left altogether to the implementation phase. This is not satisfactory, since the actual performance ofa prover depends heavily on the search plan. We give a new, abstract definition of search plan and we define precisely how the inference rules and the search plan cooperate to generate a derivation. To our knowledge, this is the first mathematical definition of search plan. In our previous work on completion procedures, we characterized completion-based theorem proving strategies by three properties: monotonicity, relevance and proof reduction. In fact, these properties capture the essential aspects of any theorem proving process. We show that they are functoriality properties: this result clarifies what part of the structure of a theory a theorem proving derivation is required to preserve. We close the paper with a comparison with related work and a discussion on further extensions of our categorical approach.