|
Descripción
|
|
|---|---|
| We present a new framework for the representation and resolution of first-order unification problems and their abstract syntax in a variable-free relational formalism which is a variant of Tarski-Givant relational algebra and Freyd’s allegories restricted to the fragment necessary to compile and execute logic programs. A decision procedure for validity of relational terms is developed, which corresponds to solving the original unification problem. The decision procedure is presented as a conditional relational-term rewriting system. A more efficient version can be obtained by tailoring certain rewriting mechanisms. There are advantages over classical unification approaches. First, inconvenient and underspecified meta-logical procedures (name clashes, substitution, etc) are captured algebraically within the framework. Second, interesting algebraic properties usually living in the meta-level spring up. Third, other unification problems are seamlessly accommodated, for instance, unification for terms with a variable-restriction operator. | |
|
Internacional
|
Si |
|
Nombre congreso
|
22nd International Workshop on Unification(UNIF'08) |
|
Tipo de participación
|
960 |
|
Lugar del congreso
|
Hagenberg, Austria |
|
Revisores
|
Si |
|
ISBN o ISSN
|
|
|
DOI
|
|
|
Fecha inicio congreso
|
18/07/2008 |
|
Fecha fin congreso
|
18/07/2008 |
|
Desde la página
|
0 |
|
Hasta la página
|
0 |
|
Título de las actas
|
Proceedings of the 22nd International Workshop on Unification (UNIF'08) |