Yet another bijection between sequent calculus and natural deduction

DOI10.1016/J.ENTCS.2015.04.007zbMATH Open1343.03042OpenAlexW2017264513WikidataQ113317807 ScholiaQ113317807MaRDI QIDQ530853FDOQ530853

Authors: 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

proof theorynatural deductionsequent calculusintuitionistic propositional logic

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The correspondence between cut-elimination and normalization
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Normalization as a homomorphic image of cut-elimination
• Title not available (Why is that?)
• A framework for proof systems

Cited In (6)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Multi-focused proofs with different polarity assignments
• Title not available (Why is that?)
• Extended Natural Deduction Images of Conversions from the System of Sequents
• An ecumenical notion of entailment
• A negationless interpretation of intuitionistic theories. I

Uses Software

• Pesca

This page was built for publication: Yet another bijection between sequent calculus and natural deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q530853)