Primal grammars and unification modulo a binary clause

3Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free