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
Conference papers

Some Issues about Proof Search in Linear Logic - abstract -

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The analysis and the automated construction of new semantic structures such as proof nets can be seen as an issue for proof-search, with some relationships with more classical and efficient search methods. The interest of such structures will be emphasized in different ways: their relationships with based-on connections provability characterizations, their use to analyse non-provability in commutative and non-commutative logics, the use of labelled proof nets to consider the linear intuitionistic provability from linear classical search. The study of completeness results is also essential to propose semantics that could have strong impact on proof-search. It will be illustrated by a revised semantics of intuitionistic linear logic, that allows to naturally establish the non-provability of some formulae.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:41:02 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098991, version 1



Didier Galmiche. Some Issues about Proof Search in Linear Logic - abstract -. Logic & Computation - LC'99, Workshop on Proofs, 1999, Edinburgh, Scotland, 36 p. ⟨inria-00098991⟩



Record views