Connection-Based Proof Search in Propositional BI Logic

  • Didier Galmiche
  • Daniel Méry
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


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.

Unable to display preview. Download preview PDF.


  1. 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. 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
  3. 3.
    W. Bibel. On matrices with connections. Journal of ACM, 28(4):633–645, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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
  5. 5.
    D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1–2):231–272, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 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. 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. 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
  9. 9.
    C. Kreitz and J. Otten. Connection-based theorem proving in classical and non-classical logics. Journal of Universal Computer Science, 5(3):88–112, 1999.zbMATHMathSciNetGoogle Scholar
  10. 10.
    P. O’Hearn. Resource interpretations, bunched implications and the αλ-calculus. In Typed Lambda Calculi and Applications, TLCA’99, LNCS 581, pages 258–279, L’Aquila, Italy, 1999.CrossRefGoogle Scholar
  11. 11.
    P.W. O’Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.CrossRefMathSciNetGoogle Scholar
  12. 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
  13. 13.
    M. E. Stickel. A unification algorithm for associative-commutative functions. Journal of ACM, 28(3):423–434, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    A. Urquhart. Semantics for relevant logic. Journal of Symbolic Logic, 37:159–169, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 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. 16.
    L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Didier Galmiche
    • 1
  • Daniel Méry
    • 1
  1. 1.LORIAUniversité Henri PoincaréVandœuvre-lès-NancyFrance

Personalised recommendations