Best-First Rippling

Rippling is a form of rewriting that guides search by only performing steps that reduce the syntactic differences between formulae. Termination is normally ensured by a measure that is decreases with each rewrite step. Because of this restriction, rippling will fail to prove theorems about, for example, mutual recursion as 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...

• Type: Conference
• Year: 2006
• Where: BIRTHDAY
• Authors: Moa Johansson, Alan Bundy, Lucas Dixon
• Keywords: Applied Computing, BIRTHDAY 2006, Ordinary Rippling, Rippling, Traditional Depth-first Rippling