Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics Publications >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/4524

This item has been viewed 9 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
BundyA_Coloured Rippling.pdf96.32 kBAdobe PDFView/Open
Title: Coloured rippling: An extension of a theorem proving heuristic
Authors: Yoshida, Tetsuya
Bundy, Alan
Green, Ian
Walsh, Toby
Basin, David
Issue Date: 1994
Journal Title: Proceedings of the Eleventh European Conference on Artificial Intelligence, Amsterdam, The Netherlands, August 8-12, 1994
Page Numbers: 85-89
Publisher: John Wiley & Sons
Abstract: Rippling is a type of rewriting developed in inductive theorem proving for removing differences between terms; the induction conclusion is annotated to mark its differences from the induction hypothesis and rippling attempts to move these differences. Until now rippling has been primarily employed in proofs where there is a single induction hypothesis.This paper describes an extension to rippling to deal with theorems with multiple hypotheses.Such theorems arise, for instance, when reasoning about data-structures like trees with multiple recursive arguments. The essential idea is to colour the annotation, with each colour corresponding to a different hypothesis. The annotation of rewrite rules used in rippling is similarly generalized so that rules propagate colours through terms. This annotation guides search so that rewrite rules are only applied if they reduce the differences between the conclusion and some of the hypotheses.We have tested this implementation on a number of problems, including two of Bledsoe’s challenge limit theorems.
URI: http://dblp.uni-trier.de/db/conf/ecai/ecai94.html
http://hdl.handle.net/1842/4524
Appears in Collections:Informatics Publications

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy