Canonical Inference for Implicational Systems

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 simplication into account.