Abstract
Proof-search (the basis of logic programming) with multiplicative inference rules, such as linear logic's ⊗R and '8L, is problematic because of the required non-deterministic splitting of resources. Similarly, searching with additive rules such as &L and ⊕R requires a non-deterministic choice between two formulae. Many strategies which resolve such non-determinism, either locally or globally, are available.
We present a characterization of a range of strategies for distributing and selecting resources in linear sequent calculus proof-search via a sequent calculus annotated with Boolean constraints. Strategies are characterized by calculations of solutions of sets of Boolean equations generated by searches. Our characterization encompasses lazy (or local), eager (or global) and intermediate (mixed local and global) strategies.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J.-M. Andreoli. Logic Programming with Focusing Proofs in Linear Logic. J. Logic Computat. 2(3), 1992.
D. Galmiche and G. Perrier. On proof normalization in Linear Logic, Theoret. Comp. Sci. 135, 67–110, 1994.
G. Gentzen. Untersuchungen über das logische Schliessen. Math. Zeit. 39, 176–210, 405–431, 1934.
J.-Y. Girard. Linear Logic. Theoret. Comp. Sci. 50, 1–102, 1987.
J.-Y. Girard. Proof-nets for Additives. Manuscript, 1994.
J. Harland, D. Pym and M. Winikoff. Programming in Lygon: An Overview. Proc. AMAST'96, M. Wirsing and M. Nivat, editors, LNCS 1101, 391–405, July, 1996.
J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Inform. and Computat. 110:2:327–365, 1994.
P. Lincoln and N. Shankar. Proof Search in First-order Linear Logic and Other Cut-free Proc. of the IEEE Symposium on Logic in Computer Science 281–292, Paris, June, 1994.
D. Miller. A multiple-conclusion meta-logic. Proc. of the IEEE Symposium on Logic in Computer Science 272–281, Paris, June, 1994.
D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. J. Logic Computat. 4:2:175–207, 1994.
D. Pym and L. Wallen. Logic Programming via Proof-valued Computations. In: ALPUK92, Proc. 4th U.K. Conference on Logic Programming, K. Broda (editor), 253–263. Springer-Verlag, Workshops in Computing Series, 1992.
T. Tammet. Proof Search Strategies in Linear Logic. J. Automat. Reas. 12:273–304, 1994.
A. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29, 1992.
M. Winikoff and J. Harland. Implementing the Linear Logic Programming Language Lygon. Proc. ILPS'95 66–80, J. Lloyd (ed.), MIT Press, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harland, J., Pym, D. (1997). Resource-distribution via Boolean constraints. In: McCune, W. (eds) Automated Deduction—CADE-14. CADE 1997. Lecture Notes in Computer Science, vol 1249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63104-6_21
Download citation
DOI: https://doi.org/10.1007/3-540-63104-6_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63104-0
Online ISBN: 978-3-540-69140-2
eBook Packages: Springer Book Archive