The Explosion Calculus

Studia Logica 108 (3):509-547 (2020)
  Copy   BIBTEX


A calculus for classical propositional sequents is introduced that consists of a restricted version of the cut rule and local variants of the logical rules. Employed in the style of proof search, this calculus explodes a given sequent into its elementary structural sequents—the topmost sequents in a derivation thus constructed—which do not contain any logical constants. Some of the properties exhibited by the collection of elementary structural sequents in relation to the sequent they are derived from, uniqueness and unique representation of formula occurrences, will be discussed in detail. Based on these properties it is suggested that a collection of elementary structural sequents constitutes the purely structural representation of the sequent from which it is obtained.



    Upload a copy of this work     Papers currently archived: 92,873

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
Proofs with monotone cuts.Emil Jeřábek - 2012 - Mathematical Logic Quarterly 58 (3):177-187.
Higher-order sequent-system for intuitionistic modal logic.Kosta Dosen - 1985 - Bulletin of the Section of Logic 14 (4):140-142.
Sequent-systems for modal logic.Kosta Došen - 1985 - Journal of Symbolic Logic 50 (1):149-168.
Cut-free double sequent calculus for S5.A. Indrzejczak - 1998 - Logic Journal of the IGPL 6 (3):505-516.
A minimal classical sequent calculus free of structural rules.Dominic Hughes - 2010 - Annals of Pure and Applied Logic 161 (10):1244-1253.
On the unity of logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
Aspects of analytic deduction.Athanassios Tzouvaras - 1996 - Journal of Philosophical Logic 25 (6):581-596.


Added to PP

35 (#468,960)

6 months
9 (#352,506)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations