Experiments with Proof Plans for Induction

Alan Bundy, F. van Harmelen, J. Hesketh, A. Smaill

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Pages (from-to)303-324
JournalJournal of Automated Reasoning
Volume7
Issue number3
DOIs
Publication statusPublished - 1991

Keywords / Materials (for Non-textual outputs)

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

Fingerprint

Dive into the research topics of 'Experiments with Proof Plans for Induction'. Together they form a unique fingerprint.

Cite this