Ordinal arithmetic: A case study for rippling in a higher order domain

Louise A Dennis, Alan Smaill

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 λ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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication14th International Conference, TPHOLs 2001 Edinburgh, Scotland, UK, September 3–6, 2001 Proceedings
PublisherSpringer Berlin Heidelberg
Pages185-200
Number of pages16
ISBN (Electronic)978-3-540-44755-9
ISBN (Print)978-3-540-42525-0
DOIs
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume2152
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Ordinal arithmetic: A case study for rippling in a higher order domain'. Together they form a unique fingerprint.

Cite this