|
Descripción
|
|
|---|---|
| Substitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a case-by-case basis, or can we turn the idea of substitution into a mathematical object? We give axioms for substitution and prove them sound and complete with respect to a canonical model. As corollaries we obtain a useful conservativity result, and prove that equality-up-to-substitution is a decidable relation on terms. These results involve subtle use of techniques both from rewriting and algebra. A special feature of our method is the use of nominal techniques. These give us access to a stronger assertion language, which includes so-called ‘freshness’ or ‘capture-avoidance’ conditions. This means that the sense in which we axiomatise substitution (and prove soundness and completeness) is particularly strong, while remaining quite general. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
FORMAL ASPECTS OF COMPUTING |
|
ISSN
|
0934-5043 |
|
Factor de impacto JCR
|
0,698 |
|
Información de impacto
|
|
|
Volumen
|
20 |
|
DOI
|
|
|
Número de revista
|
4 |
|
Desde la página
|
451 |
|
Hasta la página
|
479 |
|
Mes
|
ENERO |
|
Ranking
|
|