@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}
}

{"_id":{"_str":"53421af8ecd21cdc07000396"},"__v":14,"authorIDs":["54574b892abc8e9f37000276","5457d2032abc8e9f3700078e","545a8863b43425b772000f8b","546b8379ec3c47a5180002f9"],"author_short":["Arias, E. J. G.","Lipton, J.","Marińo, J.","Nogueira, P.","Marin, M."],"bibbaseid":"arias-lipton-mario-nogueira-marin-firstorderunificationusingvariablefreerelationalalgebra-2008","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Emilio","Jesús","Gallego"],"propositions":[],"lastnames":["Arias"],"suffixes":[]},{"firstnames":["James"],"propositions":[],"lastnames":["Lipton"],"suffixes":[]},{"firstnames":["Julio"],"propositions":[],"lastnames":["Marińo"],"suffixes":[]},{"firstnames":["Pablo"],"propositions":[],"lastnames":["Nogueira"],"suffixes":[]},{"firstnames":["Mircea"],"propositions":[],"lastnames":["Marin"],"suffixes":[]}],"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","bibtex":"@inproceedings{ ejga:unif08,\n author = {Emilio Jesús Gallego Arias and James Lipton and Julio Marińo and Pablo Nogueira and Mircea Marin},\n title = {First-order Unification Using Variable-free Relational Algebra}, \n 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},\n booktitle = {Proceedings of the 22nd International Workshop on Unification (UNIF'08)},\n month = {July 18} ,\n year = {2008}\n}\n\n\n","author_short":["Arias, E. J. G.","Lipton, J.","Marińo, J.","Nogueira, P.","Marin, M."],"key":"ejga:unif08","id":"ejga:unif08","bibbaseid":"arias-lipton-mario-nogueira-marin-firstorderunificationusingvariablefreerelationalalgebra-2008","role":"author","urls":{},"downloads":0},"bibtype":"inproceedings","biburl":"http://data.bibbase.org/provenance/httpbabellsfiupmesangelpublicationsbib/?format=bibtex","downloads":0,"keywords":[],"search_terms":["first","order","unification","using","variable","free","relational","algebra","arias","lipton","marińo","nogueira","marin"],"title":"First-order Unification Using Variable-free Relational Algebra","year":2008,"dataSources":["EuJsgsLE4BnnkifQw"]}