HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Proof nets Construction and Automated Deduction in Non-commutative Linear Logic - extended abstract -

Didier Galmiche 1 Bruno Martin
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents an algorithm for automated proof nets construction in the non-commutative multiplicative linear logic (NCMLL) that is a logic useful for applications as planning, concurrency or sequentiality. The properties of this algorithm can be proved from a recently defined graph-theoretic characterization of non-commutative proof nets. Involving simple construction principles improved in the commutative case, it induces also a new proof search method for NCMLL. Moreover the relationships between non-commutative linear logic and Lambek calculus lead to a new method for automatic construction of proof nets for this calculus.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/inria-00098604
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 5:03:53 PM
Last modification on : Wednesday, May 12, 2021 - 4:56:04 PM

Identifiers

  • HAL Id : inria-00098604, version 1

Collections

Citation

Didier Galmiche, Bruno Martin. Proof nets Construction and Automated Deduction in Non-commutative Linear Logic - extended abstract -. Electronic Notes in Theoretical Computer Science, Elsevier, 1998, 17, pp.1-20. ⟨inria-00098604⟩

Share

Metrics

Record views

42