Strong Normalisation of Cut-Elimination in Classical Logic
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
Strong Normalisation of Cut-Elimination in Classical Logic
|
| Id. |
45663473 |
| Idioma |
inglés
|
| Titulo |
Strong Normalisation of Cut-Elimination in Classical Logic |
| Autor(es) |
C. Urban Marseille France G. M. Bierman |
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.9711
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules. Keywords: Classical Logic, Cut-Elimination, Strong Normalisation, Symmetric Reducibility Candidates. |
| Tipo |
application/postscript |
| Palabras clave |
Classical Logic |
| Tipo de recurso |
Texto Narrativo
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| Formatos |
application/postscript |
| Requerimientos técnicos |
Browser: Any |
| Relación |
[IsBasedOn] http://www.cl.cam.ac.uk/~gmb/Publications/../Papers/FI.ps
[References] 10.1.1.26.6893
[References] 10.1.1.43.6938
[References] 10.1.1.46.7895
[References] 10.1.1.37.8903
[References] 10.1.1.40.173
[References] 10.1.1.132.1052
[References] 10.1.1.48.5593
[References] 10.1.1.38.7773
[References] 10.1.1.87.9046
[References] 10.1.1.116.966
[References] 10.1.1.25.5659
[References] 10.1.1.143.9815
[References] 10.1.1.100.482
[References] 10.1.1.137.8607
[References] 10.1.1.103.7736
[References] 10.1.1.104.5083
[References] 10.1.1.106.7062
[References] 10.1.1.108.8910
[References] 10.1.1.87.9762
[References] 10.1.1.91.1292
[References] 10.1.1.94.9433
[References] 10.1.1.112.5490
[References] 10.1.1.114.1507
[References] 10.1.1.122.3631
[References] 10.1.1.39.4097
[References] 10.1.1.23.9553
[References] 10.1.1.144.1803
|
| Fecha de contribución |
26-sep-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|