System description: Proof planning in higher-order logic with λClam
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.
KeywordsLogic Program System Description Hardware System Inductive Proof Automate Deduction
Unable to display preview. Download preview PDF.
- 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
- 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
- 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