- Abstract:
-
This paper reports a case study in the use of proof planning in the context of higher order syntax. Rippling is a heuristic for guiding rewriting steps in induction that has been used successfully in the proof planning inductive of proofs using first order representations. Ordinal arithmetic provides a natural set of higher order examples on which transfinite induction may be attempted using rippling. Previously Boyer-Moore style automation could not be applied to such domains. We demonstrate that a higher-order extension of the rippling heuristic is sufficient to plan such proofs automatically. Accordingly, ordinal arithmetic has been implemented in LambdaClam, a higher order proof planning system for induction, and standard undergraduate text book problems have been successfully planned with a simple extension to the standard machinery for higher order rippling and induction. We show the synthesis of a fixpoint for normal ordinal functions which demonstrates how our automation could be extended to produce more interesting results that the textbook examples tried so far.
- Copyright:
- 2001 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0040,
- author = {
Alan Smaill
and Louise Dennis
},
- title = {Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain},
- book title = {Proceedings of TPHOLs 2001 (International Conference on Theorem Proving in Higher Order Logics)},
- publisher = {Springer},
- year = 2001,
- month = {Apr},
- volume = {2152},
- pages = {185-200},
- }
|
