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.
Type de document :
Communication dans un congrès
Logic & Computation - LC'99, Workshop on Proofs, 1999, Edinburgh, Scotland, 36 p, 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00098991
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:02
Dernière modification le : mardi 24 avril 2018 - 13:34:56

Identifiants

  • HAL Id : inria-00098991, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

53