Canonical inference for implicational systems

Abstract. Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries. We investigate what canonicity means for implicational systems that are axiomatizations of Moore fam-ilies – or, equivalently, of propositional Horn theories. We build a corre-spondence between implicational systems and associative-commutative rewrite systems, give deduction mechanisms for both, and show how their respective inferences correspond. Thus, we exhibit completion pro-cedures designed to generate canonical systems that are “optimal ” for forward chaining, to compute minimal models, and to generate canoni-cal systems that are rewrite-optimal. Rewrite-optimality is a new notion of “optimality ” for implicational systems, one that takes contraction by simplification into account.