Translations from natural deduction to sequent calculus

DOI10.1002/MALQ.200310047MaRDI QIDQ4434498zbMATH OpenOpenAlexFDO

Authors Jan von Plato

Publication date 10 November 2003

Published in MLQ (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.200310047

zbMATH Keywords

intuitionistic logicnatural deductionsequent calculuscut-free derivationnormal derivation

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

• A sequent calculus isomorphic to Gentzen's natural deduction
• scientific article; zbMATH DE number 1406467
• Natural deduction with general elimination rules
• scientific article; zbMATH DE number 3275554
• Extended Natural Deduction Images of Conversions from the System of Sequents

Cited in

(20)

• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
• Monadic translation of classical sequent calculus
• On the notion of canonical derivations from open assumptions and its role in proof-theoretic semantics
• Natural deduction bottom up
• Prawitz, Proofs, and Meaning
• scientific article; zbMATH DE number 1980937 (Why is no real title available?)
• A Compressing Translation from Propositional Resolution to Natural Deduction
• Extended Natural Deduction Images of Conversions from the System of Sequents
• The elimination of maximum cuts in linear logic and BCK logic
• 2-Sequent Calculus: Intuitionism and Natural Deduction
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• Sequent calculus in natural deduction style
• An ecumenical notion of entailment
• Eight rules for implication elimination
• Natural deduction with general elimination rules
• From Gentzen to Jaśkowski and back: algorithmic translation of derivations between the two main systems of natural deduction
• scientific article; zbMATH DE number 874672 (Why is no real title available?)
• Maximum segments as natural deduction images of some cuts
• A connection between cut elimination and normalization
• A sequent calculus isomorphic to Gentzen's natural deduction

This page was built for publication: Translations from natural deduction to sequent calculus

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