Combining Logic Programming and Equation Solving

摘要

Conditional equational theories can be built into logic programming using a generalized resolution rule which calls a universal unification procedure. Such unification procedures are often defined by sound and strongly complete sets of inference rules. In other words, to resolve upon two atoms requires to show—by means of the inference rules—that the corresponding arguments of the atoms are equal under a given equational theory. In this sense, derivations with respect to resolution and the inference rules are controlled by a fixed computation rule. However, since the unification problem is undecidable for many classes of equational theories, this fixed computation rule has several drawbacks. We show that refutations with respect to resolution and sound and strongly complete sets of inference rules for conditional equational theories are independent of a computation rule. Hence, resolution and equation solving can be performed on the same le