Skip to main content
SpringerLink
Log in

A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming

  • Conference paper
  • First Online:
Logic Programming (ICLP 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2401))

Included in the following conference series:

Abstract

Higher-order logic programming languages such as Elf extend first-order logic programming in two ways: first-order terms are replaced with (dependently) typed λ-terms and the body of clauses may contain implication and universal quantification. In this paper, we describe tabled higher-order logic programming where some redundant computation is eliminated by memoizing sub-computation and re-using its result later. This work extends Tamaki and Sato’s search strategy based on memoization to the higher-order setting. We give a proof-theoretic characterization of tabling based on uniform proofs and prove soundness of the resulting interpreter. Based on it, we have implemented a prototype of a tabled logic programming interpreter for Elf.

This work was partially supported by NSF Grant CCR-9988281.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. W. Appel and A. P. Felty. A semantic model of types and machine instructions for proof-carrying code. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’ 00), pages 243–253, 2000.

    Google Scholar 

  2. I. Cervesato. A Linear Logical Framework. PhD thesis, Dipartimento di Informatica, Università di Torino, 1996.

    Google Scholar 

  3. I. Cervesato, J. S. Hodas, and F. Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1–2):133–163, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  4. I. Cervesato and F. Pfenning. A linear spine calculus. In submitted, 2001.

    Google Scholar 

  5. W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20–74, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. B. Cui, Y. Dong, X. Du, K. N. Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D. S. Warren. Logic programming and model checking. In Principles of Declarative Programming, volume 1490 of Lecture Notes in Computer Science, pages 1–20. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  7. J. Harland and D. Pym. Resource-distribution via boolean constraints. In Proceedings of the 14th International Conference on Automated Deduction (CADE-14), pages 222–236, Townsville, Australia, 1997. Springer-Verlag LNAI 1249.

    Google Scholar 

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

  9. D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321–358, 1992.

    Article  MATH  MathSciNet  Google Scholar 

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

  11. G. Nadathur and D. Miller. An overview of λProlog. In Fifth International Logic Programming Conference, pages 810–827, Seattle, Washington, 1988. MIT Press.

    Google Scholar 

  12. G. Necula and S. Rahul. Oracle-based checking of untrusted software. In 28th ACM Symposium on Principles of Programming Languages (POPL01), 2001.

    Google Scholar 

  13. L. C. Paulson. Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237–258, 1986.

    Article  MathSciNet  MATH  Google Scholar 

  14. F. Pfenning. Elf: A language for logic definition and verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, 1989. IEEE Computer Society Press.

    Google Scholar 

  15. F. Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, Netherlands, 1991.

    Google Scholar 

  16. F. Pfenning. Computation and Deduction. Cambridge University Press, 2000. In preparation. Draft from April 1997 available electronically.

    Google Scholar 

  17. F. Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, USA, 2001.

    Google Scholar 

  18. F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN’ 88 Symposium on Language Design and Implementation, pages199–208, Atlanta, Georgia, 1988.

    Google Scholar 

  19. F. Pfenning and C. Schürmann. System description: Twelf — a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202–206, Trento, Italy, 1999. Springer-Verlag LNAI 1632.

    Google Scholar 

  20. B. Pientka. Tabled higher-order logic programming. Thesis proposal, Carnegie Mellon University, 2002.

    Google Scholar 

  21. A. Roychoudhury, C. R. Ramakrishnan, and I. V. Ramakrishnan. Justifying proofs using memo tables. In International Conference on Principles and Practice of Declarative Programming(PPDP’00), pages 178–189, 2000.

    Google Scholar 

  22. K. Sagonas and T. Swift. An abstract machine for tabled execution of fixed-order stratified logic programs. ACM Transactions on Programming Languages and Systems, 20(3):586–634, 1998.

    Article  Google Scholar 

  23. H. Tamaki and T. Sato. OLD resolution with tabulation. In E.. Shapiro, editor, Proceedings of the 3rd International Conference on Logic Programming, volume 225 of Lecture Notes in Computer Science, pages 84–98. Springer, 1986.

    Google Scholar 

  24. R. Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 2000.

    Google Scholar 

  25. D. S. Warren. Programming in tabled logic programming. draft available from http://www.cs.sunysb.edu/ warren/xsbbook/book.html, 1999.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 15213, USA

    Brigitte Pientka

Authors
  1. Brigitte Pientka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Software Engineering, University of Melbourne, 221 Bouverie St., Carlton, 3053, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pientka, B. (2002). A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming. In: Stuckey, P.J. (eds) Logic Programming. ICLP 2002. Lecture Notes in Computer Science, vol 2401. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45619-8_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-45619-8_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43930-1

  • Online ISBN: 978-3-540-45619-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation