|
Descripción
|
|
|---|---|
| We present an extension of first-order predicate logic with a novel predicate ‘at t’ meaning intuitively “this term is a variable symbol”. We give simple sequent proof-rules for it, we demonstrate cut-elimination for the resulting logic, and we give a semantics for which the logic is sound and complete. Because we can now make assertions about what would normally be considered an intensional property of a term (being a variable symbol) we can now express inside the logic, properties of its terms and predicates which would normally be external to the logic. We give axiomatisations in a-logic, including of the lambda-calculus, and discuss what relevance this might have to logic programming. | |
|
Internacional
|
Si |
|
JCR del ISI
|
No |
|
Título de la revista
|
Electronic Notes in Theoretical Computer Science |
|
ISSN
|
1571-0661 |
|
Factor de impacto JCR
|
0 |
|
Información de impacto
|
|
|
Volumen
|
216 |
|
DOI
|
10.1016/j.entcs.2008.06.031 |
|
Número de revista
|
0 |
|
Desde la página
|
3 |
|
Hasta la página
|
29 |
|
Mes
|
ENERO |
|
Ranking
|
|