Proof-Search and Countermodel Generation in Propositional BI Logic

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


In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.


Induction Hypothesis Logic Programming Intuitionistic Logic Linear Logic Substructural Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


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.
    M. D’Agostino and D.M. Gabbay. A Generalization of Analytic Deduction via Labelled Deductive Systems. Part I: Basic substructural logics. Journal of Automated Reasoning, 13:243–281, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1-2):231–272, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proofsearch in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN’99, LNCS 1742, pages 101–112, Phuket, Thailand, December 1999.Google Scholar
  6. 6.
    D. Galmiche and J.M. Notin. Proof-search and proof nets in mixed linear logic. Electronic Notes in Theoretical Computer Science, 37, 2000.Google Scholar
  7. 7.
    J.Y. Girard. Linear logic: its syntax and semantics. In J.Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1995.Google Scholar
  8. 8.
    S. Ishtiaq and P. O’Hearn. Bias 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
  9. 9.
    H. Mantel and J. Otten. linTAP: A tableau prover for linear logic. In Int. Conference TABLEAUX’99, LNCS 1617, pages 216–231, Saratoga Springs, NY, USA, 1999.Google Scholar
  10. 10.
    R.K. Meyer, M.A. McRobbie, and N. Belnap. Linear analytic tableaux. In Theorem proving with analytic tableaux and related methods, TABLEAUX’95, LNCS 918, pages 278–293, St Goaram Rhein, Germany, 1995.Google Scholar
  11. 11.
    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
  12. 12.
    P.W. O’Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    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
  14. 14.
    K. Terui. Labelled tableau calculi generating simple models for substructural logics. Technical report, ILLC publications, University of Amsterdam, 1999.Google Scholar
  15. 15.
    A. Urquhart. Semantics for relevant logic. Journal of Symbolic Logic, 37:159–169, 1972.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Didier Galmiche
    • 1
  • Daniel Méry
    • 1
  1. 1.LORIA — Université Henri Poincaré, Campus ScientifiqueVandoeuvre-lès-NancyFrance

Personalised recommendations