Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1998: Automated Deduction — CADE-15 pp 129–133Cite as

System description: Proof planning in higher-order logic with λClam

  • Conference paper
  • First Online:

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

Abstract

This system description outlines the λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying higher-order proof planning to a number of types of problem is outlined, in particular the synthesis and verification of software and hardware systems. The use of a higher-order metatheory overcomes problems encountered in Clam because of its inability to reason properly about higher-order objects. λClam is written in λProlog.

The authors gratefully acknowledge the support of EPSRC grant GR/L/11724 and British Council grant ROM/889/95/70 and for the comments of their colleagues in the Mathematical Reasoning Group and of the referees.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Brisset and O. Ridoux. The architecture of an implementation of LambdaProlog: Prolog/Mali. In Proceedings of the Workshop on Implementation of Logic Programming, ILPS'94, Ithaca, NY. The MIT Press, November 1994.

    Google Scholar 

  2. A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185–253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.

    Article  MathSciNet  MATH  Google Scholar 

  3. A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.

    Google Scholar 

  4. Alan Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111–120. Springer-Verlag, 1988. Longer version available as DAI Research Paper No. 349.

    Google Scholar 

  5. A. Felty. A logic programming approach to implementing higher-order term rewriting. In L-H Eriksson et al., editors, Second International Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 135–61. Springer-Verlag, 1992.

    Google Scholar 

  6. J. T. Hesketh. Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, University of Edinburgh, 1991.

    Google Scholar 

  7. A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1–2):79–111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.

    Article  MathSciNet  MATH  Google Scholar 

  8. A. Smaill and I. Green. Higher-order annotated terms for proof search. In J. von Wright, J. Grundy, and J Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 399–414. Springer, 1996. Also available as DAI Research Paper 799.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Artificial Intelligence, Edinburgh University, 80 South Bridge, EH1 1HN, Scotland

    Julian Richardson, Alan Smaill & Ian Green

Authors
  1. Julian Richardson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alan Smaill
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ian Green
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Richardson, J., Smaill, A., Green, I. (1998). System description: Proof planning in higher-order logic with λClam. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054254

Download citation

  • DOI: https://doi.org/10.1007/BFb0054254

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation