Skip to main content

Research Repository

See what's under the surface

Advanced Search

Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain

Dennis, Louise Abigail; Smaill, Alan

Authors

Louise Abigail Dennis

Alan Smaill



Contributors

Richard J. Boulton
Editor

Paul B. Jackson
Editor

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 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.

Publication Date Jan 1, 2001
Peer Reviewed Peer Reviewed
APA6 Citation Dennis, L. A., & Smaill, A. (2001). Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. In P. B. Jackson, & R. J. Boulton (Eds.),
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information Lecture Notes in Computer SCience 2152

Files

ordinals.ps (417 Kb)
Other

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





Downloadable Citations

;