Connection-Based Proof Search in Propositional BI Logic
- 282 Downloads
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 w.r.t. intuitionistic logic and multiplicative intuitionistic linear logic, we deduce, by some restrictions, new connection-based characterizations and methods for both logics.
Unable to display preview. Download preview PDF.
- 1.P.A. Armelin and D. Pym. Bunched logic programming (extended abstract). In First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, pages 289–304, Siena, Italy, 2001.Google Scholar
- 2.V. Balat and D. Galmiche. Labelled Deduction, volume 17 of Applied Logic Series, chapter Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.Google Scholar
- 4.K. Broda, M. Finger, and A. Russo. LDS-natural deduction for substructural logics (extended abstract). Logic Journal of the IGPL, 4(3):486–489, 1996.Google Scholar
- 6.D. Galmiche and D. Méry. Proof-search and countermodel generation in propositional BI logic-extended abstract-. In 4th Int. Symp. on Theoretical Aspects of Computer Software, TACS 2001, LNCS 2215, pages 263–282, Sendai, Japan, 2001.Google Scholar
- 7.S. Ishtiaq and P. O’Hearn. BI as an assertion language for mutable data structures. In 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pages 14–26, London, UK, 2001.Google Scholar
- 8.C. Kreitz, H. Mantel, J. Otten, and S. Schmitt. Connection-based proof construction in linear logic. In 14th Int. Conference on Automated Deduction, pages 207–221, Townsville, North Queensland, Australia, 1997.Google Scholar
- 12.D. Pym. On bunched predicate logic. In 14h Symposium on Logic in Computer Science, pages 183–192, Trento, Italy, July 1999. IEEE Computer Society Press.Google Scholar
- 15.A. Voronkov. Proof-search in intuitionistic logic based on constraint satisfaction. In Int. Workshop Tableaux’96, LNAI 1071, pages 312–327, Terrasini, Italy, 1996.Google Scholar
- 16.L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.Google Scholar