Proof-search and Proof nets in Mixed Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Electronic Notes in Theoretical Computer Science Année : 2001

Proof-search and Proof nets in Mixed Linear Logic

Résumé

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.
Fichier non déposé

Dates et versions

inria-00099227 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00099227 , version 1

Citer

Didier Galmiche, Jean-Marie Notin. Proof-search and Proof nets in Mixed Linear Logic. Electronic Notes in Theoretical Computer Science, 2001, 37, pp.1-33. ⟨inria-00099227⟩
77 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More