Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:51:03 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00100790, version 1



Didier Galmiche, Daniel Méry. Connection-based proof search in propositional BI logic. 18th International Conference on Automated Deduction - CADE-18, 2002, Copenhagen/Denmark, pp.111-128. ⟨inria-00100790⟩



Record views