The Use of Explicit Plans to Guide Inductive Proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these specifications in a sorted meta-logic, we are able to reason about the conjectures to be proved and the methods available to prove them. In this way we can build proof plans of wide generality, formally account for and predict their successes and failures, apply them flexibly, recover from their failures, and learn them from example proofs. We illustrate this technique by building a proof plan based on a simple subset of the implicit proof plan embedded in the Boyer-Moore theorem prover, [Boyer & Moore 79].
Original languageEnglish
Title of host publication9th International Conference on Automated Deduction
Subtitle of host publicationArgonne, Illinois, USA, May 23–26, 1988 Proceedings
PublisherSpringer-Verlag GmbH
ISBN (Electronic)978-3-540-39216-3
ISBN (Print)978-3-540-19343-2
DOIs
Publication statusPublished - May 1988

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume310
ISSN (Print)0302-9743

Keywords / Materials (for Non-textual outputs)

  • Proof plans
  • inductive proofs
  • theorem proving
  • automatic programming
  • formal methods
  • planning

Fingerprint

Dive into the research topics of 'The Use of Explicit Plans to Guide Inductive Proofs'. Together they form a unique fingerprint.

Cite this