Skip to main content
SpringerLink
Log in

Tabling for Higher-Order Logic Programming

  • Conference paper
Automated Deduction – CADE-20 (CADE 2005)

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

Included in the following conference series:

Abstract

We describe the design and implementation of a higher-order tabled logic programming interpreter where some redundant and infinite computation is eliminated by memoizing sub-computation and re-using its result later. In particular, we focus on the table design and table access in the higher-order setting where many common operations are undecidable in general. To achieve a space and time efficient implementation, we rely on substitution factoring and higher-order substitution tree indexing. Experimental results from a wide range of examples (propositional theorem proving, refinement type checking, small-step evaluator) demonstrate that higher-order tabled logic programming yields a more robust and more powerful proof procedure.

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. Abadi, M., Cardelli, L., Curien, P.-L., Lèvy, J.-J.: Explicit substitutions. In: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, pp. 31–46. ACM, New York (1990)

    Google Scholar 

  2. Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: ACM Conference on Computer and Communications Security, pp. 52–62 (1999)

    Google Scholar 

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

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  5. Crary, K.: Toward a foundational typed assembly language. In: 30th ACM Symposiumn on Principles of Programming Languages (POPL), New Orleans, Louisisana, pp. 198–212. ACM-Press, New York (2003)

    Chapter  Google Scholar 

  6. Cui, B., Dong, Y., Du, X., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 1–20. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Davies, R., Pfenning, F.: Intersection types and computational effects. In: Proceedings of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada, pp. 198–208. ACM Press, New York (2000)

    Chapter  Google Scholar 

  8. Demoen, B., Sagonas, K.: CAT: The copying approach to tabling. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 21–36. Springer, Heidelberg (1998)

    Google Scholar 

  9. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

  10. Howe, J.M.: Two loop detection mechanisms: a comparison. In: TABLEAUX 1997. LNCAI, vol. 1227, pp. 188–200. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  11. Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, Paris, France, June 1991, pp. 255–269. MIT Press, Cambridge (1991)

    Google Scholar 

  12. Nadathur, G., Miller, D.: An overview of λProlog. In: Fifth International Logic Programming Conference, Seattle, Washington, August 1988, pp. 810–827. MIT Press, Cambridge (1988)

    Google Scholar 

  13. Necula, G., Rahul, S.: Oracle-based checking of untrusted software. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 142–154 (2001)

    Google Scholar 

  14. Necula, G., Lee, P.: Efficient representation and validation of logical proofs. In: Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS 1998), June 1998, pp. 93–104. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  16. Pfenning, F.: Elf: A language for logic definition and verified meta-programming. In: Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, June 1989, pp. 313–322. IEEE Computer Society Press, Los Alamitos (1989)

    Chapter  Google Scholar 

  17. Pfenning, F.: Unification and anti-unification in the Calculus of Constructions. In: Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 1991, pp. 74–85 (1991)

    Google Scholar 

  18. Pfenning, F., Schürmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Pientka, B.: A proof-theoretic foundation for tabled higher-order logic programming. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 271–286. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Sciences, Carnegie Mellon University, CMU-CS-03-185 (December 2003)

    Google Scholar 

  21. Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 473–487. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  22. Ramakrishnan, I.V., Rao, P., Sagonas, K., Swift, T., Warren, D.: Efficient access mechanisms for tabled logic programs. Journal of Logic Programming 38(1), 31–54 (1999)

    Article  MATH  Google Scholar 

  23. Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1853–1962. Elsevier Science Publishers B.V, Amsterdam (2001)

    Chapter  Google Scholar 

  24. Sagonas, K., Swift, T.: 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 

  25. Tamaki, H., Sato, T.: OLD resolution with tabulation. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 84–98. Springer, Heidelberg (1986)

    Google Scholar 

  26. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, Available as Technical Report CMU-CS-99-167 (Sep. 1999)

    Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, McGill University,  

    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. Technical University of Catalonia, Barcelona

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pientka, B. (2005). Tabling for Higher-Order Logic Programming. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_5

Download citation

  • DOI: https://doi.org/10.1007/11532231_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28005-7

  • Online ISBN: 978-3-540-31864-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation