On narrowing, refutation proofs and constraints

Abstract

We develop a proof technique for dealing with narrowing and refutational theorem proving in a uniform way, clarifying the exact relationship between the existing results in both fields and allowing us to obtain several new results. Refinements of narrowing (basic, LSE, etc.) are instances of the technique, but are also defined here for arbitrary (possibly ordering and/or equality constrained or not yet convergent or saturated) Horn clauses, and shown compatible with simplification and other redundancy notions. By narrowing modulo equational theories like AC, compact representations of solutions, expressed by AC-equality constraints, can be obtained. Computing AC-unifiers is only needed at the end if one wants to "uncompress" such a constraint into its (doubly exponentially many) concrete substitutions.