Natural deduction with general elimination rules
From MaRDI portal
Publication:1407508
DOI10.1007/s001530100091zbMath1021.03050OpenAlexW2060230835MaRDI QIDQ1407508
Publication date: 16 September 2003
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s001530100091
sequent calculusnormalizationconjunction eliminationcut-free derivationderivations with cutsimplication eliminationstructure of derivations in natural deduction
Related Items (44)
NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION ⋮ Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective) ⋮ Gentzen's Proof Systems: Byproducts in a Work of Genius ⋮ General-elimination harmony and the meaning of the logical constants ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ ON FLATTENING ELIMINATION RULES ⋮ BILATERAL RELEVANT LOGIC ⋮ An Alternative Natural Deduction for the Intuitionistic Propositional Logic ⋮ Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications ⋮ Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules ⋮ A faithful and quantitative notion of distant reduction for generalized applications ⋮ From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction ⋮ A note on harmony ⋮ Type checking and typability in domain-free lambda calculi ⋮ Focusing in Linear Meta-logic ⋮ Bilateralism in proof-theoretic semantics ⋮ A logic inspired by natural language: quantifiers as subnectors ⋮ A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION ⋮ Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization ⋮ The polarized \(\lambda\)-calculus ⋮ Proof Terms for Generalized Natural Deduction ⋮ On harmony and permuting conversions ⋮ Harmony in multiple-conclusion natural-deduction ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ On the unity of duality ⋮ In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs ⋮ Normal proofs, cut free derivations and structural rules ⋮ The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony ⋮ A survey of nonstandard sequent calculi ⋮ A framework for proof systems ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Prawitz, Proofs, and Meaning ⋮ Cut Elimination, Substitution and Normalisation ⋮ Inversion Principles and Introduction Rules ⋮ Meaning in Use ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Deriving Natural Deduction Rules from Truth Tables ⋮ INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES ⋮ Normal derivations and sequent derivations ⋮ The normalization theorem for extended natural deduction ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ ON THE NOTION OF CANONICAL DERIVATIONS FROM OPEN ASSUMPTIONS AND ITS ROLE IN PROOF-THEORETIC SEMANTICS ⋮ Varieties of linear calculi ⋮ Normalisation and subformula property for a system of classical logic with Tarski's rule
This page was built for publication: Natural deduction with general elimination rules
