Observatorio de I+D+i UPM

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
S2i 2019 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)