The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

PhD Thesis #9111

Title:Using Middle-Out Reasoning to Guide Inductive Theorem Proving
Date: 1991
Abstract:Techniques derived from proof theory for logic alone have been insufficient as a basis for efficient, elegant automatic theorem proving. They concentrate on syntax, neglecting both strategy for particular domains and classes of problem, and guidance from modelling human mathematicians. A novel technique suggested by Bundy, developing ideas from Ernst & Newell, is to reason "middle-out". Often, the overall structure of proof may be known, but its details must be fleshed out according to the individual theorem. Conventional search might use heuristic guidance to backtrack over all possibilities. Middle-out reasoning uses variables as place-holders for parameters still to be chosen. These place-holders become instantiated by the requirements of the subsequent proof. Decisions which would multiply the search space are postponed until more information is available. This is an exciting development in search control, making extensive use of strategic guidance and harnessing tools from human reasoning. This thesis reports research on its use for synthesis of tail recursive functions from corresponding naive functions and for proofs requiring generalisation. it enables the development of a unified framework for generalisation. An existing proof planning and development system based on Martin-Loef Type Theory, Oyster/CLAM, is used as a vehicle, augmented by higher order unification.

[Search These Pages] [DAI Home Page] [Comment]