Edinburgh Research Explorer

Best-First Rippling

Research output: Chapter in Book/Report/Conference proceedingChapter

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
Pages83-100
Number of pages18
ISBN (Electronic)978-3-540-37902-7
ISBN (Print)978-3-540-37901-0
DOIs
StatePublished - 2006

Publication series

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

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.

Download statistics

No data available

ID: 7553264