Resource data
Classical Logic = Fibred MLL
Hughes, Dominic
Location:
http://arxiv.org/abs/math/0504028
This paper represents classical propositional proofs as *combinatorial
proofs*, which are more abstract than proof nets: superposition
(contraction/weakening) is modelled mathematically, as a lax form of fibration,
rather than syntactically (as in proof nets, which involve contraction and
weakening nodes). A combinatorial proof is a `fibred' multiplicative linear
proof net, hence the slogan in the title. Cut elimination retains its richness
from sequent calculus: its non-determinism does not collapse to become
confluent. [Note: this is merely a 2-page synopsis, accepted for a short
presentation at Logic in Computer Science '05.]
Belongs to: arXiv
Descargar SCORM
¡Sea el primero en solicitar este recurso!
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
Users rating
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
Detalles del recurso
|
Classical Logic = Fibred MLL
|
| Id. |
21051641 |
| Titulo |
Classical Logic = Fibred MLL |
| Autor(es) |
Hughes, Dominic |
| Location |
http://arxiv.org/abs/math/0504028
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
This paper represents classical propositional proofs as *combinatorial
proofs*, which are more abstract than proof nets: superposition
(contraction/weakening) is modelled mathematically, as a lax form of fibration,
rather than syntactically (as in proof nets, which involve contraction and
weakening nodes). A combinatorial proof is a `fibred' multiplicative linear
proof net, hence the slogan in the title. Cut elimination retains its richness
from sequent calculus: its non-determinism does not collapse to become
confluent. [Note: this is merely a 2-page synopsis, accepted for a short
presentation at Logic in Computer Science '05.] |
| Palabras clave |
Mathematics - 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í
|
| Requerimientos técnicos |
Browser: Any |
| Fecha de contribución |
26-feb-2007 |
| Contacto |
|
|