In resolution theorem proving as well as in its descendant, logic programming, we are frequently confronted with binary clauses causing lengthy or infinite computations because of their self-resolvents. In this paper we investigate unification modulo a binary clause, which can be used as a short cut through loops of the form L → R. For a certain class of binary clauses we show that (i) its unification problem is decidable and (ii) the unifiers can be finitely schematized. This is done by first reducing the binary clauses to a simpler form and then employing primal grammars [12]. Our work extends results obtained in the context of cycle unification.
CITATION STYLE
Salzer, G. (1994). Primal grammars and unification modulo a binary clause. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 814 LNAI, pp. 282–295). Springer Verlag. https://doi.org/10.1007/3-540-58156-1_20
Mendeley helps you to discover research relevant for your work.