Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
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 n...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Springer
2001
|
| Online Access: | https://eprints.nottingham.ac.uk/339/ |
| _version_ | 1848790394646560768 |
|---|---|
| author | Dennis, Louise Abigail Smaill, Alan |
| author2 | Boulton, Richard J. |
| author_facet | Boulton, Richard J. Dennis, Louise Abigail Smaill, Alan |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:11:55Z |
| format | Conference or Workshop Item |
| id | nottingham-339 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:55Z |
| publishDate | 2001 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3392020-05-04T20:32:43Z https://eprints.nottingham.ac.uk/339/ Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain Dennis, Louise Abigail Smaill, Alan 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. Springer Boulton, Richard J. Jackson, Paul B. 2001 Conference or Workshop Item PeerReviewed 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. |
| spellingShingle | Dennis, Louise Abigail Smaill, Alan Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title | Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title_full | Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title_fullStr | Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title_full_unstemmed | Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title_short | Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain |
| title_sort | ordinal arithmetic: a case study for rippling in a higher order domain |
| url | https://eprints.nottingham.ac.uk/339/ |