Proof-Search and Countermodel Generation in Propositional BI Logic
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.
KeywordsInduction Hypothesis Logic Programming Intuitionistic Logic Linear Logic Substructural Logic
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
- 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.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.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.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.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.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
- 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.K. Terui. Labelled tableau calculi generating simple models for substructural logics. Technical report, ILLC publications, University of Amsterdam, 1999.Google Scholar