Abstract
The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, ⊥, the challenge consists in dealing with BI’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI’s pointer logic and for which BI is complete
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
V. Balat and D. Galmiche. Labelled Deduction, in Volume 17 of Applied Logic Series, Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.
M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer Verlag, 1990.
D. M. Gabbay. Labelled Deductive Systems. OUP, 1996.
D. Galmiche and D. Méry. Proof-search and countermodel generation in propositional BI logic-extended abstract-. In 4th Int. Symposium on Theoretical Aspects of Computer Software, TACS 2001, LNCS 2215, 263–282, Sendai, Japan, 2001. Full version submitted.
J. Harland and D. Pym. Resource-distribution via Boolean Constraints (Extended Abstract). In 14th Int. Conference on Automated Deduction, CADE-12, LNAI 814, 222–236, Townsville, Queensland, Australia, July 1997. Full version to appear in ACM ToCL, 2003.
Y. Lafont. The finite model property for various fragments of linear logic. J. Symb. Logic 62(4):1202–1208, 1997.
P. Lincoln. Deciding provability of linear logic formulas. In Advances in Linear Logic, J.-Y. Girard, Y. Lafont and L. Regnier (editors), Cambridge Univ. Press, 1995, 109–122.
S. Ishtiaq and P. O’Hearn. BI as an assertion language for mutable data structures. In Proc. 28th ACM Symp. on Principles of Prog. Langs., POPL 2001, 14–26, London, UK, 2001.
P. O’Hearn and J. Reynolds and H. Yang. Local Reasoning about Programs that Alter Data Structures. In Proc. 15th Int. Workshop on Computer Science Logic, CSL’01, LNCS 2142, 1–19, Paris, 2001.
P. W. O’Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999.
M. Okada and K. Terui. Completeness proofs for linear logic based on proof search method (preliminary report). In Type theory and its applications to computer systems, 57–75, RIMS, Kyoto University, 1998.
D. Pym. On bunched predicate logic. In Proc. 14th Symposium on Logic in Computer Science, 183–192, Trento, Italy, July 1999. IEEE Computer Society Press.
D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers, 2002. To appear; preprint available at http://www.cs.bath.ac.uk/~pyni/recent.html.
D. J. Pym, P. W. O’Hearn and H. Yang. Possible Worlds and Resources: The Semantics of BI. Manuscript, http://www.cs.bath.ac.uk/~pym/recent.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D., Méry, D., Pym, D. (2002). Resource Tableaux. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive