Yet another bijection between sequent calculus and natural deduction

DOI10.1016/J.ENTCS.2015.04.007MaRDI QIDQ530853zbMATH OpenOpenAlexWikidataFDO

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

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A framework for proof systems
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Normalization as a homomorphic image of cut-elimination
• The correspondence between cut-elimination and normalization

Cited in

(6)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Multi-focused proofs with different polarity assignments
• scientific article; zbMATH DE number 1980937 (Why is no real title available?)
• Extended Natural Deduction Images of Conversions from the System of Sequents
• An ecumenical notion of entailment
• A negationless interpretation of intuitionistic theories. I

Describes a project that uses

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)