Structural Cut Elimination in Linear 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
|
|
|
Structural Cut Elimination in Linear Logic
|
| Id. |
46430448 |
| Idioma |
inglés
|
| Titulo |
Structural Cut Elimination in Linear Logic |
| Autor(es) |
Frank Pfenning December
Frank Pfenning
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.1153
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. The computational content of this proof is a non-deterministic algorithm for cut elimination which is amenable to an elegant implementation in Elf. We show this implementation in detail. This work was supported by NSF Grant CCR-9303383 The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of NSF or the U.S. government. Keywords: Linear Logic, Cut Elimination, Logical Framework Contents 1 Introduction 1 2 CLL: A Traditional Sequent Calculus for Linear Logic 1 3 LV: Another Sequent Calculus for Linear Logic 3 4 Linear Proof Terms 8 5 Representation in LF 11 5.1 Formulas : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 11 5.2 Pro...
|
| Tipo |
application/postscript
|
| Palabras clave |
Linear 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://foxnet.cs.cmu.edu/people/fp/papers/cutlin94.ps.gz
[References] 10.1.1.21.5854
[References] 10.1.1.50.9674
[References] 10.1.1.105.9987
[References] 10.1.1.28.2136
[References] 10.1.1.16.2984
[References] 10.1.1.25.1142
[References] 10.1.1.40.3910
[References] 10.1.1.51.3753
|
| Fecha de contribución |
28-jul-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
