Skip to main content
SpringerLink
Log in
Book cover

Computational Logic: Logic Programming and Beyond pp 105–137Cite as

Higher-Order Computational Logic

  • Chapter
  • First Online:

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

Abstract

This paper presents a case for the use of higher-order logic as a foundation for computational logic. A suitable polymorphically-typed, higher-order logic is introduced and its syntax and proof theory briefly described. In addition, a metric space of closed terms suitable for knowledge representation purposes is presented. The approach to representing individuals is illustrated with some examples, as is the technique of programming with abstractions. The paper concludes by placing the results in the wider context of previous and current research in the use of higher-order logic in computational 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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. P.B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.

    Google Scholar 

  2. A.F. Bowers, C. Giraud-Carrier, and J.W. Lloyd. Classification of individuals with complex structure. In P. Langley, editor, Machine Learning: Proceedings of the Seventeenth International Conference (ICML2000), pages 81–88. Morgan Kaufmann, 2000.

    Google Scholar 

  3. A.F. Bowers, C. Giraud-Carrier, and J.W. Lloyd. A knowledge representation framework for inductive learning. Available at http://csl.anu.edu.au/~jwl, 2001.

  4. A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

    Article  MATH  MathSciNet  Google Scholar 

  5. T.G. Dietterich, R.H. Lathrop, and T. Lozano-Pérez. Solving the multiple instance problem with axis-parallel rectangles. Artificial Intelligence, 89:31–71, 1997.

    Article  MATH  Google Scholar 

  6. M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  7. M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994.

    Article  MathSciNet  Google Scholar 

  8. M. Hanus (ed.). Curry: An integrated functional logic language. Available at http://www.informatik.uni-kiel.de/~curry.

  9. S. Peyton Jones and J. Hughes (editors). Haskell98: A non-strict purely functional language. Available at http://haskell.org/.

  10. R. A. Kowalski. Predicate logic as a programming language. In Information Processing 74, pages 569–574, Stockholm, 1974. North Holland.

    Google Scholar 

  11. J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, second edition, 1987.

    Google Scholar 

  12. J.W. Lloyd. Programming in an integrated functional and logic language. Journal of Functional and Logic Programming, 1999(3), March 1999.

    Google Scholar 

  13. J.W. Lloyd. Knowledge representation, computation, and learning in higher-order logic. Available at http://csl.anu.edu.au/~jwl, 2001.

  14. T.M. Mitchell. Machine Learning. McGraw-Hill, 1997.

    Google Scholar 

  15. G. Nadathur and D.A. Miller. Higher-order logic programming. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, The Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 499–590. Oxford University Press, 1998.

    Google Scholar 

  16. D.A. Wolfram. The Clausal Theory of Types. Cambridge University Press, 1993.

    Google Scholar 

  17. Home page of Machine Learning Group, The University of York. http://www.cs.york.ac.uk/mlg/.

Download references

Author information

Authors and Affiliations

  1. Computer Sciences Laboratory Research School of Information Sciences and Engineering, Australian National University, Australia

    John W. Lloyd

Authors
  1. John W. Lloyd
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Cyprus, 75 Kallipoleos St., 1678, Nicosia, Cyprus

    Antonis C. Kakas

  2. Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen’s Gate, London, SW7 2BZ, UK

    Fariba Sadri

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Lloyd, J.W. (2002). Higher-Order Computational Logic. In: Kakas, A.C., Sadri, F. (eds) Computational Logic: Logic Programming and Beyond. Lecture Notes in Computer Science(), vol 2407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45628-7_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-45628-7_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43959-2

  • Online ISBN: 978-3-540-45628-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation