Ultimate Normal Forms for Parallelized Natural Deductions

DOI10.1093/JIGPAL/10.3.299MaRDI QIDQ3147433zbMATH OpenOpenAlexFDO

Authors Neil Tennant

Publication date 18 September 2002

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/08496ca396c40e1413c5454738df46a9cce74f79

zbMATH Keywords

cut-eliminationdeductive relevanceHauptsatzintuitionistic relevant logicnatural deductionnormal formsnormalization theoremparallelized elimination rulesreduction proceduresequent calculus

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Recommendations

• scientific article; zbMATH DE number 3275554
• scientific article; zbMATH DE number 1406467
• The normalization theorem for extended natural deduction
• Two normalizations for naturald deductions in sequent style
• scientific article; zbMATH DE number 874672

Cited in

(14)

• The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony
• Analytic rules for mereology
• scientific article; zbMATH DE number 3853043 (Why is no real title available?)
• scientific article; zbMATH DE number 1222496 (Why is no real title available?)
• Hyper natural deduction for Gödel logic -- a natural deduction system for parallel reasoning
• scientific article; zbMATH DE number 874672 (Why is no real title available?)
• 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
• Two normalizations for naturald deductions in sequent style
• Proof Terms for Generalized Natural Deduction
• Core Type Theory
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Eight rules for implication elimination
• Comments on the contributions

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Ultimate Normal Forms for Parallelized Natural Deductions

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