Edinburgh Research Explorer

Experiments with Proof Plans for Induction

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

Documents

Original languageEnglish
Pages (from-to)303-324
JournalJournal of Automated Reasoning
Volume7
Issue number3
DOIs
StatePublished - 1991

Abstract

The technique of proof plans, is outlined. This technique is used to guide
automatic inference in order to avoid a combinatorial explosion. Empirical research to test this technique in the domain of theorem proving by mathematical induction is described. Heuristics, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specied in a meta-logic, and plan formation has been used to reason with these specications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster's search space. The success rate on the standard theorems is high. These preliminary results are very encouraging.

    Research areas

  • Theorem proving, mathematical induction, search, Combinatorial explosion, Proof plans, tactics, Planning

Download statistics

No data available

ID: 401788