Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1997: Automated Deduction—CADE-14 pp 222–236Cite as

Resource-distribution via Boolean constraints

Extended abstract

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1249))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.-M. Andreoli. Logic Programming with Focusing Proofs in Linear Logic. J. Logic Computat. 2(3), 1992.

    Google Scholar 

  2. D. Galmiche and G. Perrier. On proof normalization in Linear Logic, Theoret. Comp. Sci. 135, 67–110, 1994.

    Article  MathSciNet  Google Scholar 

  3. G. Gentzen. Untersuchungen über das logische Schliessen. Math. Zeit. 39, 176–210, 405–431, 1934.

    Article  Google Scholar 

  4. J.-Y. Girard. Linear Logic. Theoret. Comp. Sci. 50, 1–102, 1987.

    Article  MathSciNet  Google Scholar 

  5. J.-Y. Girard. Proof-nets for Additives. Manuscript, 1994.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Inform. and Computat. 110:2:327–365, 1994.

    Article  MathSciNet  Google Scholar 

  8. 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.

    Google Scholar 

  9. D. Miller. A multiple-conclusion meta-logic. Proc. of the IEEE Symposium on Logic in Computer Science 272–281, Paris, June, 1994.

    Google Scholar 

  10. D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. J. Logic Computat. 4:2:175–207, 1994.

    Article  MathSciNet  Google Scholar 

  11. 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.

    Google Scholar 

  12. T. Tammet. Proof Search Strategies in Linear Logic. J. Automat. Reas. 12:273–304, 1994.

    Article  MathSciNet  Google Scholar 

  13. A. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29, 1992.

    Google Scholar 

  14. M. Winikoff and J. Harland. Implementing the Linear Logic Programming Language Lygon. Proc. ILPS'95 66–80, J. Lloyd (ed.), MIT Press, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Royal Melbourne Institute of Technology, England

    James Harland

  2. Queen Mary and Westfield College, University of London, England

    David Pym

Authors
  1. James Harland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Pym
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

William McCune

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation