A New Deconstructive Logic: 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
|
|
|
A New Deconstructive Logic: Linear Logic
|
| Id. |
41621615 |
| Idioma |
inglés
|
| Titulo |
A New Deconstructive Logic: Linear Logic |
| Autor(es) |
Vincent Danos,Jean-baptiste Joinet,Harold Schellinx
|
| Localización |
http://citeseer.ist.psu.edu/186498.html
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
The main concern of this paper is the design of a noetherian and
confluent normalization for LK
2
(that is, classical second order predicate
logic presented as a sequent calculus).
The method we present is powerful: since it allows us to recover
as fragments formalisms as seemingly different as Girard's LC and
Parigot's ¯, FD ([10, 12, 29, 33]), delineates other viable systems
as well, and gives means to extend the Krivine/Leivant paradigm of
`programming-with-proofs' ([24, 25]) to classical logic; it is painless:
since we reduce strong normalization and confluence to the same properties
for linear logic (for non-additive proof nets, to be precise) using
appropriate embeddings (so-called decorations); it is unifying: it organizes
known solutions in a simple pattern that makes apparent the
how and why of their making.
A comparison of our method to that of embedding LK into LJ
(intuitionistic sequent calculus) brings to the fore the latter's defects
for these `deconstructive purposes'...
|
| Tipo |
ps
|
| Palabras clave |
Vincent Danos,Jean-baptiste Joinet,Harold Schellinx A New Deconstructive Logic: Linear Logic
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
unrestricted |
| Formatos |
ps
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] ftp://ftp.logique.jussieu.fr/pub/distrib/joinet/DanosJoinetSchellinx/decostringopolaro.ps.Z
|
| Fecha de contribución |
31-mar-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
