Rippling in a Higher Order Setting

Overview

Rippling[Bundy et al 05] is a key proof planning technique used principally to automate proof by mathematical induction. There are a number of differing theories of rippling[Hutter and Kohlhase 00, Dixon and Fleuriot 04], especially where it can account for higher order properties, and a number of variations of the underlying technique[Yoshida et. al 94, Smaill and Green 95,Ireland and Bundy 96]. It is also a technique which is complex and error-prone both to implement and also to describe (I am aware of at least one major error in a paper on the subject and a number of minor ones).

Rippling is an extremely powerful automated reasoning technique, and in particular may help significantly in the automation of synthesis proofs and middle-out reasoning. However there are a number of challenges to be overcome before it can be easily adopted. The technique is in bad need of formalisation to clarify the ambiguities and to establish the relationships between different theories. Theoretical and experimental comparative work is required to evaluate the scope of variant theories. Experimental work is also required to evaluate how different rippling variants interact in practice and to detail their implementation in a clear fashion. It is highly likely that further variants will be discovered as a natural consequence of this work.

I was involved with work to extend rippling to higher-order logics and a paper on this (with Dr. Alan Smaill (Edinburgh) and Dr. Ian Green (Telelogic)) is currently under revision for the Journal of Automated Reasoning. This will be the last outstanding major rippling theory to be documented.

I'm working with Dr. Lucas Dixon (Edinburgh) to formalise the theory, extend it to cover the notion of sinks and validate the relationships between different theories of rippling.

I have also been working on the implementation of rippling variants within the new higher-order theories. This will hopefully both fill in the detail of how these variants work in practice, how they interact with different theories and, hopefully, illuminate new areas of study.

People

Funding

EPSRC grant GR/S01771/01: The Integration and Interaction of Multiple Mathematical Reasoning Processes.

Publications

Embeddings as a Higher Order Representation of Annotations for Rippling

Bibliography

Bundy et al 05: A. Bundy, D. Basin, D. Hutter and A. Ireland. Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science 56, Cambridge University Press, 2005.
Dixon and Fleuriot 04: L. Dixon and J. D. Fleuriot. Higher Order Rippling in IsaPlanner. Theorem Proving in Higher Order Logics 2004 (TPHOLs 2004). LNCS 3223. Springer, 2004.
Hutter and Kohlhase 00: D. Hutter and M. Kohlhase. Managing Structural Information by Higher Ordered Colored Unification. Journal of Automated Reasoning, 25(2), 125-164, 2000.
Ireland and Bundy 96: A. Ireland and A. Bundy. Productive use of Failure in Inductive Proof. Journal of Automated Reasoning, 16(1-2), pp. 79-111. 1996.
Smaill and Green 95: A. Smaill and I. Green. Automating the synthesis of functional programs, Research Paper 777, Department of Artificial Intelligence, University of Edinburgh, 1995
Smaill and Green 96: A. Smaill and I. Green. Higher-order Annotated terms for Proof search. J. von Wright, J. Grundy and J. Harrison (eds) 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96). LNCS 1275, pp.399-414, Springer, 1996.
Basin and Walsh 96: D. Basin and T. Walsh. A Calculus for and Termination of Rippling, Journal of Automated Reasoning, 16(1-2), pp. 147-180. 1996
Yoshida et. al. 94: T. Yoshida, A. Bundy, I. Green, T. Walsh and D. Basin. Coloured Rippling: An extension of a Theorem Proving heuristic. A. G. Cohn (ed) Proceedings of ECAI-94. pp. 85-89. John Wiley, 1994.