Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computational Logic

CL 2000: Computational Logic — CL 2000 pp 254–268Cite as

Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic

  • Conference paper
  • First Online:

  • 597 Accesses

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

Abstract

A key property in the definition of logic programming languages is the completeness of goal-directed proofs. This concept originated in the study of logic programming languages for intuitionistic logic in the (single-conclusioned) sequent calculus LJ, but has subsequently been adapted to multiple-conclusioned systems such as those for linear logic. Given these developments, it seems interesting to investigate the notion of goal-directed proofs for a multiple-conclusioned sequent calculus for intuitionistic logic, in that this is a logic for which there are both single-conclusioned and multiple-conclusioned systems (although the latter are less well known). In this paper we show that the language obtained for the multiple-conclusioned system differs from that for the single-conclusioned case, show how hereditary Harrop formulae can be recovered, and investigate contraction-free fragments of the logic.

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. Journal of Logic and Computation, 2(3), 1992.

    Google Scholar 

  2. J.-M. Andreoli and R. Pareschi. Linear Objects: Logical Processes with Built-in Inheritance. In David H. D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 496–510, Jerusalem, 1990. The MIT Press.

    Google Scholar 

  3. K. Clark. Negation as Failure. In H. Gallaie and J. Minker, editors, Logic and Databases, pages 293–323. Plenum Press, 1978.

    Google Scholar 

  4. R. Dyckhoff. Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57:795–807, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  5. R. Dyckhoff. A Deterministic Terminating Sequent Calculus for Godel-Dummett logic. Logic Journal of the IGPL, 7:319–326, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  6. D. Galmiche and G. Perrier. On Proof Normalisation in Linear Logic. Theoretical Computer Science, 135:67–110, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  7. G. Gentzen. Untersuchungen üiber das logische Schliessen. Math. Zeit., 39:176–210,405-431, 1934.

    Article  MATH  MathSciNet  Google Scholar 

  8. J. Harland. On Normal Forms and Equivalence for Logic Programs. In Krzysztof Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 146–160, Washington, DC, 1992. ALP, MIT Press.

    Google Scholar 

  9. J. Harland. A Proof-Theoretic Analysis of Goal-Directed Provability. Journal of Logic and Computation, 4(1):69–88, January1994.

    Google Scholar 

  10. J. Harland. On Goal-Directed Provability in Classical Logic. Computer Languages, 23:161–178, 1997.

    Article  MATH  Google Scholar 

  11. J. Harland, D. Pym, and M. Winikoff. Programming in Lygon: An Overview. In M. Wirsing, editor, Lecture Notes in Computer Science, pages 391–405. Springer, July1996.

    Google Scholar 

  12. J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, 110(2):327–365, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  13. N. Kobayash and A. Yonezawa. ACL-A Concurrent Linear Logic Programming Paradigm. In Dale Miller, editor, Logic Programming-Proceedings of the 1993 International Symposium, pages 279–294, Vancouver, Canada, 1993. The MIT Press.

    Google Scholar 

  14. T. Lutovac and J. Harland. Towards the Automation of the Design of Logic Programming Languages. Technical Report 97-30, Department of Computer Science, RMIT, 1997.

    Google Scholar 

  15. D. Miller. Forum: A Multiple-Conclusion Specification Logic. Theoretical Computer Science, 165(1):201–232, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  16. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  17. J. Minker and A. Rajasekar. A Fixpoint Semantics for Disjunctive Logic Programs. Journal of Logic Programming, 9(1):45–74, July1990.

    Google Scholar 

  18. G. Nadathur. Uniform Provability in Classical Logic. Journal of Logic and Computation, 8(2):209–230, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  19. D. Pym and J. Harland. A Uniform Proof-theoretic Investigation of Linear Logic Programming. Journal of Logic and Computation, 4(2): 175–207, April1994.

    Google Scholar 

  20. E. Ritter, D. Pym, and L. Wallen. On the Intuitionistic Force of Classical Search, to appear in Theoretical Computer Science, 1999.

    Google Scholar 

  21. P. Volpe. Concurrent Logic Programming as Uniform Linear Proofs. In G. Levi and M. Rodríguez-Artalejo, editors, Proceedings of the Conference on Algebraic and Logic Programming, pages 133–149. Springer, 1994.

    Google Scholar 

  22. Lincoln Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990.

    Google Scholar 

  23. M. Winikoff. Logic Programming with Linear Logic. PhD thesis, University of Melbourne, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Royal Melbourne Institute of Technology, GPO Box 2476V, Melbourne, 3001, Australia

    James Harland, Tatjana Lutovac & Michael Winikoff

Authors
  1. James Harland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tatjana Lutovac
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael Winikoff
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. The Australian National University, Australia

    John Lloyd

  2. Simon Fraser University, Canada

    Veronica Dahl

  3. Universität Koblenz, Germany

    Ulrich Furbach

  4. The University of Birmingham, UK

    Manfred Kerber

  5. University of Manchester, UK

    Kung-Kiu Lau

  6. The Pennsylvania State University, USA

    Catuscia Palamidessi

  7. Universidade Nova de Lisboa, Portugal

    Luís Moniz Pereira

  8. The Hebrew University of Jerusalem, Israel

    Yehoshua Sagiv

  9. The University of Melbourne, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Harland, J., Lutovac, T., Winikoff, M. (2000). Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-44957-4_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67797-0

  • Online ISBN: 978-3-540-44957-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation