article

Resource-distribution via Boolean constraints

Authors:

David PymAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 4, Issue 1

Pages 56 - 90

https://doi.org/10.1145/601775.601778

Published: 01 January 2003 Publication History

Abstract

We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications (BI). We give an algebraic method for calculating the distribution of the side-formulæ in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems.

References

[1]

Andreoli, J.-M. 1992. Logic programming with focusing proofs in linear logic. J. Logic Computat. 2, 3, 297--347.

[2]

Andreoli, J.-M. 2001. Focussing and proof construction. Ann. Pure Appl. Logic 107, 1-3, 131--163.

[3]

Armelín, P. and Pym, D. 2001. Bunched logic programming (extended abstract). In Proceedings of IJCAR 2001. Lecture Notes in Artificial Intelligence 2083. Springer-Verlag, Berlin, Germany, 289--304.

[4]

Cervesato, I., Hodas, J. S., and Pfenning, F. 2000. Efficient resource management for linear logic proof search. Theoret. Comput. Sci. 232, 1--2 (Feb.). Special issue on Proof Search in Type-Theoretic Languages, D. Galmiche and D. Pym, editors.

[5]

Gabbay, D. 1996. Labelled Deductive Systems: Principles and Applications, Vol. 1: Basic Principles. Oxford University Press, Oxford, U.K.

[6]

Galmiche, D. 2000. Connection methods in linear logic and proof nets construction. Theoret. Comput. Sci. 232, 1-2, 231--272.

[7]

Galmiche, D. and Méry, D. 2001. Proof-search and countermodel generation in propositional bi logic (extended abstract). In Fourth International Symposium on Theoretical Aspects of Computer Software, TACS 2001, Sendai, Japan. Lecture Notes in Computer Science, vol. 2215, Berlin, Germany, 263--282.

[8]

Galmiche, D. and Méry, D. In press. Semantic labelled tableaux for propositional BI, I. J. Logic Computat.

[9]

Galmiche, D., Méry, D., and Pym, D. 2002. Resource tableaux (extended abstract). In Proceedings of CSL 2002, J. Bradfield, Ed. Lecture Notes in Computer Science, vol. 2471. Springer-Verlag, Berlin, Germany, 183--199.

[10]

Girard, J.-Y. 1987. Linear logic. Theoret. Comput. Sci. 50, 1--102.

[11]

Girard, J.-Y. 1994. Proof-Nets for Additives. Manuscript. Laboratoire de Mathematique Discrète, CNRS, Marseille, France.

[12]

Harland, J. and Pym, D. 1997. Resource-distribution via Boolean constraints (extended abstract). In Proceedings of the International Conference on Automated Deduction (CADE-14), W. McCune, Ed. Lecture Notes in Computer Science, vol. 1249. Springer-Verlag, Berlin, Germany, 222--236.

[13]

Harland, J., Pym, D., and Winikoff, M. 1996. Programming in Lygon: An overview. In Proceedings of the International Conference on Algebraic Methodology and Software Technology (AMAST), M. Wirsing and M. Nivat, Eds. Lecture Notes in Computer Science, vol. 1101. Springer-Verlag, Berlin, Germany, 391--405.

[14]

Hodas, J. and Miller, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Inform. Computat. 110, 2, 327--365.

[15]

Kripke, S. 1965. Semantical analysis of intuitionistic logic. In Formal Systems and Recursive Functions, J. Crossley and M. Dummett, Eds. North Holland, Amsterdam, The Netherlands, 92--130.

[16]

O'Hearn, P. and Pym, D. 1999. The logic of bunched implications. Bull. Symbol. Logic 5, 2 (June), 215--244.

[17]

Pym, D. 1999. On bunched predicate logic. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science (Trento, Italy). IEEE Computer Society, Los Alamitos, CA, 183--192.

[18]

Pym, D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series, vol. 26. Kluwer, Dordrecht, The Netherlands.

[19]

Pym, D. and Harland, J. 1994. A uniform proof-theoretic investigation of linear logic programming. J. Logic Computat. 4, 2 (Apr.), 175--207.

[20]

Pym, D., O'Hearn, P., and Yang, H. 2000. Possible worlds and resources: the semantics of BI. To appear: Theoretical Computer Science, 2003. Preprint available at www.bath.ac.uk&sim;cssdjp.

[21]

Read, S. 1988. Relevant Logic. Blackwell, London, U.K.

[22]

Restall, G. 2000. An Introduction to Substructural Logics. Routledge, London, U.K., and New York, NY.

[23]

Tammet, T. 1994. Proof search strategies in linear logic. J. Automat. Reasoning 12, 3, 273--304.

[24]

Troelstra, A. 1992. Lectures on Linear Logic. CSLI Lecture Notes No. 29, CSLI Publications, Stanford, CA.

[25]

Urquhart, A. 1972. Semantics for relevant logics. J. Symbol. Logic 37, 1, 159--169.

[26]

Winikoff, M. and Harland, J. 1995. Implementing the linear logic programming language lygon. In Proceedings of the International Logic Programming Symposium (Portland), J. Lloyd, Ed. MIT Press, Cambridge, MA, 66--80.

Cited By

Gheorghiu APym D(2023)Defining Logical Systems via Algebraic Constraints on ProofsJournal of Logic and Computation10.1093/logcom/exad065Online publication date: 24-Nov-2023
https://doi.org/10.1093/logcom/exad065
Gheorghiu ADocherty SPym D(2023)Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource SemanticsSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_23(833-875)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_23
Pym D(2019)Resource semanticsACM SIGLOG News10.1145/3326938.33269406:2(5-41)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1145/3326938.3326940
Show More Cited By

Index Terms

Resource-distribution via Boolean constraints
1. Computing methodologies
2. Theory of computation
  1. Logic
    1. Constraint and logic programming
    2. Proof theory

Recommendations

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Modal μ-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-...
Introduction to Cirquent Calculus and Abstract Resource Semantics* This material is based upon work supported by the National Science Foundation under Grant No. 0208816, and 2005 Summer Research Grant from Villanova University.

This article introduces a refinement of the sequent calculus approach called cirquent calculus. Roughly speaking, the difference between the two is that, while in Gentzen-style proof trees sibling (or cousin, etc.) sequents are disjoint and independent ...
Sequential Dynamic Logic

We introduce a substructural propositional calculus of Sequential Dynamic Logic that subsumes a propositional part of dynamic predicate logic, and is shown to be expressively equivalent to propositional dynamic logic. Completeness of the calculus with ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 4, Issue 1

January 2003

147 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/601775

Issue’s Table of Contents

Copyright © 2003 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2003

Published in TOCL Volume 4, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
434
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 22 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gheorghiu APym D(2023)Defining Logical Systems via Algebraic Constraints on ProofsJournal of Logic and Computation10.1093/logcom/exad065Online publication date: 24-Nov-2023
https://doi.org/10.1093/logcom/exad065
Gheorghiu ADocherty SPym D(2023)Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource SemanticsSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_23(833-875)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_23
Pym D(2019)Resource semanticsACM SIGLOG News10.1145/3326938.33269406:2(5-41)Online publication date: 22-Apr-2019
https://dl.acm.org/doi/10.1145/3326938.3326940
Kamide N(2016)Bunched sequential informationJournal of Applied Logic10.1016/j.jal.2016.02.00315:C(150-170)Online publication date: 1-May-2016
https://dl.acm.org/doi/10.1016/j.jal.2016.02.003
Lutovac THarland J(2013)Detection and analysis of some redundancies in linear logic sequent proofsJournal of Logic and Computation10.1093/logcom/ext00724:1(187-232)Online publication date: 4-Apr-2013
https://doi.org/10.1093/logcom/ext007
Kamide N(2013)Temporal BI: Proof system, semantics and translationsTheoretical Computer Science10.1016/j.tcs.2013.04.029492(40-69)Online publication date: Jun-2013
https://doi.org/10.1016/j.tcs.2013.04.029
Dixon LSmaill ATsang T(2009)Plans, Actions and Dialogues Using Linear LogicJournal of Logic, Language and Information10.1007/s10849-008-9079-018:2(251-289)Online publication date: 1-Apr-2009
https://dl.acm.org/doi/10.1007/s10849-008-9079-0
Galmiche DMéry DPym D(2005)The semantics of BI and resource tableauxMathematical Structures in Computer Science10.1017/S096012950500485815:6(1033-1088)Online publication date: 1-Dec-2005
https://dl.acm.org/doi/10.1017/S0960129505004858
Donnelly KGibson TKrishnaswami NMagill SPark S(2005)The Inverse Method for the Logic of Bunched ImplicationsLogic for Programming, Artificial Intelligence, and Reasoning10.1007/978-3-540-32275-7_31(466-480)Online publication date: 2005
https://doi.org/10.1007/978-3-540-32275-7_31
Lutovac THarland J(2005)A redundancy analysis of sequent proofsProceedings of the 14th international conference on Automated Reasoning with Analytic Tableaux and Related Methods10.1007/11554554_15(185-200)Online publication date: 14-Sep-2005
https://dl.acm.org/doi/10.1007/11554554_15
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents