CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI
From MaRDI portal
Publication:5024505
DOI10.1017/S1755020320000015zbMath1485.03233arXiv2001.00662MaRDI QIDQ5024505
Publication date: 26 January 2022
Published in: The Review of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2001.00662
sequent calculus; normalization; natural deduction; cut-elimination; Curry-Howard isomorphism; proof terms
03F05: Cut-elimination and normal-form theorems
03F07: Structure of proofs
03F03: Proof theory in general (including proof-theoretic semantics)
Related Items
Uses Software
Cites Work
- Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective)
- On sequence-conclusion natural deduction systems
- Existential instantiation and normalization in sequent natural deduction
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Untersuchungen über das logische Schliessen. II
- Definitional reflection and basic logic
- A natural extension of natural deduction
- Normalization theorems for full first order classical natural deduction
- Basic logic: reflection, symmetry, visibility
- Inversion Principles and Introduction Rules
- Deriving Natural Deduction Rules from Truth Tables
- Cut-elimination and redundancy-elimination by resolution
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item