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

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

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item