Informatics Report Series


Report   

EDI-INF-RR-0849


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Best-First Rippling
Authors: Moa Johansson ; Alan Bundy ; Lucas Dixon
Date:Aug 2006
Publication Title:Reasoning, Action and Interaction in AI theories and Systems
Publisher:Springer Verlag
Volume No:4155 Page Nos:81-98
Abstract:
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.
Links To Paper
1st Link
Bibtex format
@Misc{EDI-INF-RR-0849,
author = { Moa Johansson and Alan Bundy and Lucas Dixon },
title = {Best-First Rippling},
publisher = {Springer Verlag},
year = 2006,
month = {Aug},
volume = {4155},
pages = {81-98},
url = {http://dream.inf.ed.ac.uk/projects/bfrippling/bfrippling.pdf},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh