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.
People
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.
Publications
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.
pdf
Links
Web-page maintained by
Moa Johansson
