In *Proceedings of the 22nd International Workshop on Unification (UNIF'08)*, July 18, 2008.

abstract bibtex

abstract bibtex

We propose a new unification algorithm in the CET+OC+DC theory using the variable-free relational calculus, formalism in which first order logic programs are represented and executed. In this context, two terms are unifiable when their relational representations have a nonempty intersection. For this purpose a rewriting system for computing normal forms of those intersections has been defined from a standard theory of relations extended with an axiomatization of functorial term-formers. For this system, we characterize normal forms and prove confluence and termination of rewriting, thus resulting in a decision procedure. Substitution gets replaced by intersection propagation, term clashes are captured with a simple rewriting system and occurs check translates to compatibility of term sequences. The presented system suggests some interesting results, such as the posibility of developing a new rewriting technique and the algebraic formalization of all the meta-logical concepts involved in unification

@inproceedings{ ejga:unif08, author = {Emilio Jesús Gallego Arias and James Lipton and Julio Marińo and Pablo Nogueira and Mircea Marin}, title = {First-order Unification Using Variable-free Relational Algebra}, abstract = {We propose a new unification algorithm in the CET+OC+DC theory using the variable-free relational calculus, formalism in which first order logic programs are represented and executed. In this context, two terms are unifiable when their relational representations have a nonempty intersection. For this purpose a rewriting system for computing normal forms of those intersections has been defined from a standard theory of relations extended with an axiomatization of functorial term-formers. For this system, we characterize normal forms and prove confluence and termination of rewriting, thus resulting in a decision procedure. Substitution gets replaced by intersection propagation, term clashes are captured with a simple rewriting system and occurs check translates to compatibility of term sequences. The presented system suggests some interesting results, such as the posibility of developing a new rewriting technique and the algebraic formalization of all the meta-logical concepts involved in unification}, booktitle = {Proceedings of the 22nd International Workshop on Unification (UNIF'08)}, month = {July 18} , year = {2008} }

Downloads: 0