Resource Graphs and Countermodels in Resource Logics

Didier Galmiche 1 Daniel Méry 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this abstract we emphasize the role of a semantic structure called dependency graph in order to study the provability in some resource-sensitive logics, like the Bunched Implications Logic (BI) or the Non-commutative Logic (NL). Such a semantic structure is appropriate to capture the particular interactions between different kinds of connectives (additives and multiplicatives in BI and commutatives and non-commutatives in NL) during proof-search and mainly to provide countermodels in case of non-provability. We illustrate the key points with a tableau method for BI logic and present tools, namely BILL and CheckBI, dedicated for respectively countermodel generation and verification in this logic.
Type de document :
Communication dans un congrès
IJCAR 2004 Workshop W1 on Disproving - Non-Theorems, Non-validity, Non-Provability, 2004, Cork/Ireland, 2004
Liste complète des métadonnées

https://hal.inria.fr/inria-00100048
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:43
Dernière modification le : mardi 24 avril 2018 - 13:36:38

Identifiants

  • HAL Id : inria-00100048, version 1

Collections

Citation

Didier Galmiche, Daniel Méry. Resource Graphs and Countermodels in Resource Logics. IJCAR 2004 Workshop W1 on Disproving - Non-Theorems, Non-validity, Non-Provability, 2004, Cork/Ireland, 2004. 〈inria-00100048〉

Partager

Métriques

Consultations de la notice

79