MRG home page · Research · Publications · Projects · Software · People

Best-First Rippling

Project Description

Rippling is restricted to only allow rewrite steps that preserve the skeleton and decrease the ripple measure to ensure termination. As a result, rippling will fail to solve proofs about for example mutual recursion where non-skeleton preserving steps are necessary for the proof to succeed. Best-first rippling is and extension to rippling where these restrictions has been recast as heuristic scores for use in best-first search. If nothing better is available, previously illegal steps can be considered, making best-first rippling more flexible than ordinary depth-first rippling. We have implemented best-first rippling in the IsaPlanner system together with a mechanism for caching proof-states that help remove symmetries in the search space. Our experiments show that the implementation of best-first rippling is faster than IsaPlanner's version of traditional depth-first rippling, and solves a range of problems where ordinary rippling fails.

Experimental Results

Below are the complete list of experimental results on IsaPlanner's benchmarks and our additional test set for best-first rippling, along with the theory-files that were used.


This work started as the honours project of UG4 student Moa Johansson in 2004/2005, supervised by Alan Bundy and Lucas Dixon. It was developed further by Moa Johansson with funding from EPSRC Platform Grant GR/S01771/01.


Best-First Rippling. Johansson, M, Bundy, A. and Dixon, L. In O. Stock and M. Schaerf (Eds.): Reasoning, Action and Interaction in AI theories and Systems: Essays dedicated to Luigia Carlucci Aiello, LNAI 4155, pp. 83-100, 2006. Springer-Verlag Berlin.


Web-page maintained by Moa Johansson
Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.