Best-First Rippling

Moa Johansson, Alan Bundy, Lucas Dixon

Research output: Chapter in Book/Report/Conference proceedingChapter


Rippling is a form of rewriting that guides search by only performing steps that reduce the differences between formulae. Termination is normally ensured by a defined measure that is required to decrease with each step. Because of these restrictions, rippling will fail to prove theorems about, for example, mutual recursion where steps that temporarily increase the differences are necessary. Best-first rippling is an extension to rippling where the restrictions have 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 rippling. We have implemented best-first rippling in the IsaPlanner system together with a mechanism for caching proof-states that helps remove symmetries in the search space, and machinery to ensure termination based on term embeddings. Our experiments show that the implementation of best-first rippling is faster on average than IsaPlanner’s version of traditional depth-first rippling, and solves a range of problems where ordinary rippling fails.
Original languageEnglish
Title of host publicationReasoning, Action and Interaction in AI Theories and Systems
Subtitle of host publicationEssays Dedicated to Luigia Carlucci Aiello
EditorsOliviero Stock, Marco Schaerf
PublisherSpringer Berlin Heidelberg
Number of pages18
ISBN (Electronic)978-3-540-37902-7
ISBN (Print)978-3-540-37901-0
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Best-First Rippling'. Together they form a unique fingerprint.

Cite this