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

  • Julian Richardson
  • Alan Smaill
  • Ian Green
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


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.


Logic Program System Description Hardware System Inductive Proof Automate Deduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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.MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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. 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. 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. 6.
    J. T. Hesketh. Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, University of Edinburgh, 1991.Google Scholar
  7. 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.MathSciNetCrossRefzbMATHGoogle Scholar
  8. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Julian Richardson
    • 1
  • Alan Smaill
    • 1
  • Ian Green
    • 1
  1. 1.Department of Artificial IntelligenceEdinburgh UniversityScotland

Personalised recommendations