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

Dennis, Louise Abigail; Smaill, Alan

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.

Citation

Dennis, L. A., & Smaill, A. Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. Presented at 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001)

• Conference Name: 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001)
• Publication Date: Jan 1, 2001
• Deposit Date: Dec 8, 2005
• Publicly Available Date: Oct 9, 2007
• Peer Reviewed: Peer Reviewed
• Public URL: https://nottingham-repository.worktribe.com/output/1023303
• Additional Information: Lecture Notes in Computer SCience 2152