Natural deduction with general elimination rules
From MaRDI portal
Publication:1407508
DOI10.1007/s001530100091zbMath1021.03050MaRDI 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 calculus; normalization; conjunction elimination; cut-free derivation; derivations with cuts; implication elimination; structure of derivations in natural deduction
03F05: Cut-elimination and normal-form theorems
Related Items
AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ, From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction, The normalization theorem for extended natural deduction, Prawitz, Proofs, and Meaning, Cut Elimination, Substitution and Normalisation, Inversion Principles and Introduction Rules, Meaning in Use, Deriving Natural Deduction Rules from Truth Tables, 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, In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs, A new connective in natural deduction, and its application to quantum computing, Proof Terms for Generalized Natural Deduction, Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective), A note on harmony, Bilateralism in proof-theoretic semantics, A logic inspired by natural language: quantifiers as subnectors, On harmony and permuting conversions, General-elimination harmony and the meaning of the logical constants, Type checking and typability in domain-free lambda calculi, A framework for proof systems, The \(\lambda \)-calculus and the unity of structural proof theory, Normal derivations and sequent derivations, The polarized \(\lambda\)-calculus, Varieties of linear calculi, Normalisation and subformula property for a system of classical logic with Tarski's rule, Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization, Harmony in multiple-conclusion natural-deduction, 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, Strong normalization of classical natural deduction with disjunctions, On the unity of duality, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION, Gentzen's Proof Systems: Byproducts in a Work of Genius, ON FLATTENING ELIMINATION RULES, BILATERAL RELEVANT LOGIC, An Alternative Natural Deduction for the Intuitionistic Propositional Logic, A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION, Focusing in Linear Meta-logic, INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
