Incorporating equality into logic programming via surface deduction (Q1087023)

In this account the authors exploit the idea of a special deduction mechanism for logic programming called surface-deduction, henceforth s- deduction for short. They claim that this kind of deduction mechanism copes successfully with the problem of finding a refutation for any set of Horn clauses which is unsatisfiable in standard equational theory. To apply s-deduction correctly, arbitrary Horn clauses to be resolved upon are subjected to transformation into special Horn clauses labelled ''flat clauses''. This flattening also takes appropriate care of the prevailing symmetric property of equality in decomposing input clauses into flat ones. A flat clause satisfies the following structure constraints: Only variables are allowed as arguments for non-equality predicates and at most one non-variable subterm, constructed merely upon variable subterms, occurring always on the right hand side of equality predicates. Flattening is proved to be a sound, complete and terminating closure-operation on arbitrary Horn clauses. S-deduction operates on these flat clauses according to three resolution rules, coined surface resolution, surface factoring and compression, all of them preserving the flatness property of the clauses they are applied to. S-deduction's soundness and completeness in the presence of standard equality is formally shown. Both of them remain valid even for sets of Horn clauses non-incorporating equality at all. Again special lemma-based credit is given to the important and computationally troublesome symmetric property of equality. Further on s-deduction evolves as an extension of Colmerauer's approach in PROLOG II to tune efficiency tackling the problem of unification of certain nonunifiable terms by introducing the standard equality axioms. Thus the detection of non-unifiability caused by conflicts of constants or deduction cycles is rendered more feasible and even provides valuable and applicable means for control whereever and whenever appropriate. Run- time complexity can be reduced to linear progression by initiating cycle detection at the end of s-deduction.