On proof normalization in linear logic

DOI10.1016/0304-3975(94)00105-7zbMath0815.03033OpenAlexW2094047447MaRDI QIDQ1342248

Didier Galmiche, Guy Perrier

Publication date: 11 January 1995

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01297755/file/tcs1994.pdf

zbMATH Keywords

linear logicproof normalizationpermutability properties of inference rulesproof- theoretic foundation for automated deduction in linear logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (12)

From multiple sequent for additive linear logic to decision procedures for free lattices ⋮ A PSPACE-complete fragment of second-order linear logic ⋮ Non-commutative logic. III: Focusing proofs. ⋮ A Tableau Method for the Lambek Calculus based on a Matrix Characterization ⋮ Proofs as computations in linear logic ⋮ Relating state-based and process-based concurrency through linear logic (full-version) ⋮ Representing scope in intuitionistic deductions ⋮ Connection-based proof construction in linear logic ⋮ Resource-distribution via Boolean constraints ⋮ Connection methods in linear logic and proof nets construction ⋮ Proof-search in type-theoretic languages: An introduction ⋮ A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Computational interpretations of linear logic
• Constructive system for automatic program synthesis
• Program development in constructive type theory
• Planar and braided proof-nets for multiplicative linear logic with mix
• Proof strategies in linear logic
• Generating plans in linear logic. I: Actions as proofs
• Logic Programming with Focusing Proofs in Linear Logic
• Logic programming with sequent systems
• From petri nets to linear logic

This page was built for publication: On proof normalization in linear logic