Connection-based proof search in propositional BI logic

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 : We present a connection-based characterization of propositional BI (logic of bunched implications), a logic combining linear and intuitionistic connectives. This logic, with its sharing interpretation, has been recently used to reason about mutable data structures and needs proof search methods. Our connection-based characterization for BI, is based on standard notions but involves, in a specific way, labels and constraints in order to capture the interactions between connectives during the proof-search. As BI is conservative wrt intuitionistic logic and multiplicative intuitionistic linear logic, we deduce, by some restrictions, new connection-based characterizations and methods for both logics.
Type de document :
Communication dans un congrès
A. Voronkov. 18th International Conference on Automated Deduction - CADE-18, 2002, Copenhagen/Denmark, Springer Verlag, 2392, pp.111-128, 2002, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100790
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:51:03
Dernière modification le : mardi 24 avril 2018 - 13:32:50

Identifiants

  • HAL Id : inria-00100790, version 1

Collections

Citation

Didier Galmiche, Daniel Méry. Connection-based proof search in propositional BI logic. A. Voronkov. 18th International Conference on Automated Deduction - CADE-18, 2002, Copenhagen/Denmark, Springer Verlag, 2392, pp.111-128, 2002, Lecture Notes in Computer Science. 〈inria-00100790〉

Partager

Métriques

Consultations de la notice

85