Equality and abductive residua for Horn clauses (Q689280)

This paper presents an approach, called surface deduction, to introduce equality axioms into Horn clause logic in a way to avoid the entailing inefficiency that comes with their unrestricted use. In general, surface deduction refers to a family of transformational methods for reasoning with a theory of equality. A set of input clauses is first transformed to a flat form and symmetrized. The deduction process then proceeds using linear input resolution for Horn clauses, together with a limited use of factoring and a new rule called compression. The flat form of clauses is preserved by the deduction rules. The main effect of flattening is to make the term structure of the clause directly accessible to deduction. Furthermore, surface deduction has proven to be a valuable, analytical tool for understanding the role of equality in abductive reasoning. Additionally, up until now, it is the only nontrivial method for logic programming with equality that can be put to efficient use for this kind of reasoning with little or no loss of explanatory power. However, to use surface deduction in practice on a large scale, it must be enhanced, since the flattening procedure can cause substantial increase in the number of resolution steps, in search complexity and lose most of the advantages of unification. One can retain the advantages of unification and its generalizations by interpreting the set of equalities in the body of a clause as a directed graph or hypergraph. Here, the concise presentation of surface deduction, its characteristics and ramifications provide amble theoretical evidence for the status of this particular deductive inference method. The techniques that have been successful in refutation oriented logic programming should be amenable to be integrated with the ideas proposed to yield an abductively complete and efficient system.