Memorias de investigación
Research Publications in journals:
First-order Unification Using Variable-free Relational Algebra
Year:2010

Research Areas
  • Information technology and adata processing

Information
Abstract
We present a framework for the representation and resolution of first-order unification problems and their abstract syntax in a variable-free relational formalism which is an executable variant of the Tarski-Givant relation algebra and of Freyd's allegories restricted to the fragment necessary to compile and run logic programs. We develop a decision procedure for validity of relational terms, which corresponds to solving the original unification problem. The decision procedure is carried out by a conditional relational-term rewriting system. There are advantages over classical unification approaches. First, cumbersome and underspecified meta-logical procedures (name clashes, substitution, etc.) and their properties (invariance under substitution of ground terms, equality's congruence with respect to term forming, etc.) are captured algebraically within the framework. Second, other unification problems can be accommodated, for example, existential quantification in the logic can be interpreted as a new operation whose effect is to formalize the costly and error prone handling of fresh names (renaming apart).
International
Si
JCR
Si
Title
LOGIC JOURNAL OF THE IGPL
ISBN
1367-0751
Impact factor JCR
0,32
Impact info
Volume
10.1093/jigpal/jzq011
Journal number
From page
1
To page
25
Month
MAYO
Ranking
Participants
  • Autor: Emilio Jesús Gallego Arias UPM
  • Autor: Julio Mariño Carballo UPM
  • Autor: James Lipton Wesleyan University
  • Autor: Pablo Nogueira Iglesias UPM

Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa