Observatorio de I+D+i UPM

Memorias de investigación
Artículos en revistas:
First-order Unification Using Variable-free Relational Algebra
Año:2010
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
Descripción
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).
Internacional
Si
JCR del ISI
Si
Título de la revista
LOGIC JOURNAL OF THE IGPL
ISSN
1367-0751
Factor de impacto JCR
0,32
Información de impacto
Volumen
DOI
10.1093/jigpal/jzq011
Número de revista
Desde la página
1
Hasta la página
25
Mes
MAYO
Ranking
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Emilio Jesús Gallego Arias (UPM)
  • Autor: Julio Mariño Carballo (UPM)
  • Autor: James Lipton (Wesleyan University)
  • Autor: Pablo Nogueira Iglesias (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2021 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)