|
Descripción
|
|
|---|---|
| In informal mathematical discourse (such as the text of a paper on theoretical computer science) we often reason about equalities involving binding of object-variables. We find our- selves writing assertions involving meta-variables and capture-avoidance constraints on where object-variables can and cannot occur free. Formalising such assertions is problematic because the standard logical frameworks cannot express capture-avoidance constraints directly. In this paper we make the case for extending the logic of equality with meta-variables and capture-avoidance constraints, to obtain `nominal algebra¿. We use nominal techniques that allow for a direct formalisation of meta-level assertions, while remaining close to informal practice. We investigate proof-theoretical properties, we provide a sound and complete semantics in nominal sets, and we compare and contrast our design decisions with other possibilities leading to similar systems. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
JOURNAL OF LOGIC AND COMPUTATION |
|
ISSN
|
0955-792X |
|
Factor de impacto JCR
|
0,536 |
|
Información de impacto
|
|
|
Volumen
|
19 |
|
DOI
|
doi:10.1093/logcom/exp033 |
|
Número de revista
|
6 |
|
Desde la página
|
1455 |
|
Hasta la página
|
1508 |
|
Mes
|
DICIEMBRE |
|
Ranking
|
|