Annals of Pure and Applied Logic 164 (6):702-732 (2013)

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2012.05.007
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,558
Through your library

References found in this work BETA

The Structure of Multiplicatives.Vincent Danos & Laurent Regnier - 1989 - Archive for Mathematical Logic 28 (3):181-203.
A Compact Representation of Proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
Locality for Classical Logic.Kai Brünnler - 2006 - Notre Dame Journal of Formal Logic 47 (4):557-580.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

A New Correctness Criterion for Cyclic Proof Nets.V. Michele Abrusci & Elena Maringelli - 1998 - Journal of Logic, Language and Information 7 (4):449-459.
Completeness of MLL Proof-Nets W.R.T. Weak Distributivity.Jean-Baptiste Joinet - 2007 - Journal of Symbolic Logic 72 (1):159 - 170.
Interpolation in Fragments of Classical Linear Logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
Proof Nets and the Complexity of Processing Center Embedded Constructions.Mark Johnson - 1998 - Journal of Logic, Language and Information 7 (4):433-447.
Proof and Canonical Proof.Bernhard Weiss - 1997 - Synthese 113 (2):265-284.
Advances in Linear Logic.Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.) - 1995 - Cambridge University Press.
Canonical Rules.Emil Jeřábek - 2009 - Journal of Symbolic Logic 74 (4):1171 - 1205.
A Proof–Theoretic Study of the Correspondence of Hybrid Logic and Classical Logic.H. Kushida & M. Okada - 2006 - Journal of Logic, Language and Information 16 (1):35-61.


Added to PP index

Total views
64 ( #148,565 of 2,348,582 )

Recent downloads (6 months)
1 ( #512,295 of 2,348,582 )

How can I increase my downloads?


My notes