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

Connection proof search methods in Linear Logic and proof nets construction

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper we present proof search methods related with matrix (or connection) characterization of provability for fragments of Linear Logic (LL) and their relationships with automated proof and proof net construction. Non-classical logics as intuitionistic and linear logics are used in various branches of computer science and in many of these applications automated proof methods are needed. In LL the notion of proof net provides a nice, graphical representation of proofs (without some syntactical bureaucracy) and some works emphasized, for instance, the importance of proof nets to analyze evaluation strategies for proof normalization (and thus for computation) taking into account some concurrency and parallelism. We propose here a based on connection characterization of Multiplicative Linear Logic (MLL) and consequently a connection based proof search method that has the nice property to simultaneously construct a proof net (and also a sequent proof) which can be useful within proof environments. From these results, we expect to consider provability and proof nets construction in other LL fragments that are logical foundations of type-theoretic languages.
Document type :
Journal articles
Complete list of metadata

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


  • HAL Id : inria-00098601, version 1



Didier Galmiche. Connection proof search methods in Linear Logic and proof nets construction. Theoretical Computer Science, Elsevier, 1998, 30 p. ⟨inria-00098601⟩



Record views