Yet another bijection between sequent calculus and natural deduction

DOI10.1016/j.entcs.2015.04.007zbMath1343.03042OpenAlexW2017264513WikidataQ113317807 ScholiaQ113317807MaRDI QIDQ530853

Cecilia Englander, Gilles Dowek, Edward Hermann Haeusler

Publication date: 1 August 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.04.007

zbMATH Keywords

sequent calculusproof theorynatural deductionintuitionistic propositional logic

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

An ecumenical notion of entailment ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ Multi-focused proofs with different polarity assignments

Uses Software

• Pesca

Cites Work

• A framework for proof systems
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item