Connection Methods in Linear Logic and Proof Nets Construction Generation in Mixed Logics

Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We study proof-search in mixed logics like the logic of Bunched Implications (BI) or Mixed Linear Logic (MLL), with the aim to build proofs or counter-models. We illustrate the different problems and some based-on semantics solutions from the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI is the basis of new foundations for Computer Science applications (logic programming, reasoning about mutable data structures). We present a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We then study the construction of tableaux and the extraction of countermodels from the proofs of completeness and of the finite model property. Relationships with proof-search methods in MLL are analyzed.
Type de document :
Communication dans un congrès
Semantic Foundations of Proof-search, 2001, Schloss Dagsthul/Germany, 2001
Liste complète des métadonnées

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

Identifiants

  • HAL Id : inria-00100575, version 1

Collections

Citation

Didier Galmiche. Connection Methods in Linear Logic and Proof Nets Construction Generation in Mixed Logics. Semantic Foundations of Proof-search, 2001, Schloss Dagsthul/Germany, 2001. 〈inria-00100575〉

Partager

Métriques

Consultations de la notice

113