Edinburgh Research Explorer

Using failure to guide inductive proof

Research output: Book/ReportBook

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://homepages.inf.ed.ac.uk/rbf/MY_DAI_OLD_FTP/rp613.pdf
Original languageEnglish
PublisherUniversity of Edinburgh, Department of Artificial Intelligence
StatePublished - 1992

Abstract

Lemma discovery and generalization are two of the ma jor hurdles in automating inductive proof. This paper addresses aspects of these related problems. We build upon rippling, a heuristic which plays a pivotal role in guiding inductive proof. Rippling provides a high-level explanation of how to control the search for a proof. We demonstrate how this high-level explanation can be exploited productively when a proof attempt fails. In particular we show how failure can be used to focus the search for lemmas and generalizations.

Download statistics

No data available

ID: 15514913