Proof-search and Proof nets in Mixed Linear Logic

Didier Galmiche 1 Jean-Marie Notin 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper we study how to design proof-search methods for the multiplicative fragment of Mixed Linear Logic which combines both commutative and non-commutative connectives. After an analysis of the interaction and relationships between these connectives, we propose two different proof-search algorithms, both based on the construction of labelled proof nets. The labels allow in the former to fix some constraints to satisfy during the proof net search and in the latter to propagate some informations useful to guide and control the search. Such based-on proof nets methods are useful to efficiently detect the non-provability and could lead to the generation of some countermodels.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2001, 37, pp.1-33
Liste complète des métadonnées

https://hal.inria.fr/inria-00099227
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:52:00
Dernière modification le : jeudi 11 janvier 2018 - 06:20:14

Identifiants

  • HAL Id : inria-00099227, version 1

Collections

Citation

Didier Galmiche, Jean-Marie Notin. Proof-search and Proof nets in Mixed Linear Logic. Electronic Notes in Theoretical Computer Science, Elsevier, 2001, 37, pp.1-33. 〈inria-00099227〉

Partager

Métriques

Consultations de la notice

121