2005/04/01 by Dominic Hughes, Hughes, Dominic
Computer Science · Mathematics · #03B05 #03F52 #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.LO #msc:03B05 #msc:03F52
paper · pdf · doi:10.48550/arxiv.math/0504028
2 pages. Accepted for short presentation at Logic in Computer Science '05
arxiv created 2005/04/01 · openalex publication_date 2005/04/01 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.]