Classical Logic = Fibred MLL
| dc.creator | Hughes, Dominic | |
| dc.date | 2005-04-01 | |
| dc.date.accessioned | 2026-07-07T05:18:44Z | |
| dc.date.available | 2026-07-07T05:18:44Z | |
| dc.description | 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.] | |
| dc.description | 2 pages. Accepted for short presentation at Logic in Computer Science '05 | |
| dc.identifier | https://arxiv.org/abs/math/0504028 | |
| dc.identifier | http://arxiv.org/abs/math/0504028 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/74767 | |
| dc.subject | Logic | |
| dc.subject | 03B05; 03F52 | |
| dc.title | Classical Logic = Fibred MLL | |
| dc.type | text |