Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
Contribuinte(s) |
Boulton, Richard J. Jackson, Paul B. |
---|---|
Data(s) |
2001
|
Resumo |
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 proof planning inductive 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 lambda-clam, a higher order proof planning system for induction, and standard undergraduate text book problems have been successfully planned. We show the synthesis of a fixpoint for normal ordinal functions which demonstrates how our automation could be extended to produce more interesting results than the textbook examples tried so far. |
Formato |
application/postscript |
Identificador |
http://eprints.nottingham.ac.uk/339/1/ordinals.ps Dennis, Louise Abigail and Smaill, Alan (2001) Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. In: 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), 2001, Edinburgh, UK. |
Idioma(s) |
en |
Publicador |
Springer |
Relação |
http://eprints.nottingham.ac.uk/339/ |
Tipo |
Conference or Workshop Item PeerReviewed |