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

PhD Thesis #8911

Title:An Improved Method for the Mechanisation of Inductive Proof
Authors:Stevens,A
Date: 1989
Presented:
Keywords:
Abstract:If a large-scale software system is to be dependable and maintainable it must be correct. That is, it must satisfy its specification. Unfortunately, ensuring correctness typically requires extensive formal proofs. The complexity of these proofs, which usually require the application of mathematical induction, is such that their manual construction is prohibitively expensive. The wide-spread development of dependable and maintainable software is therefore, at least in part predicated on the construction of automatic theorem provers capable of mechanising these proofs. An important problem that any such automatic theorem prover must solve is the construction induction schemata that will allow inductive proofs to succeed - appropriate induction schemata. This thesis further develops existing work on the construction of appropriate inductions due to Boyer and Moore. A rational reconstruction of Boyer and Moore's algorithm for constructing dual inductions is used to develop an enhanced algorithm suitable for a wide variety of logics. This algorithm, which is simpler and more effective than the original, is then developed into an explicit heuristic theory of appropriate inductions. This theory provides the well-defined, refutable, theoretical basis for the development of improved automatic theorem provers that Boyer and Moore's work omits. A prototype implementation of the reconstructed algorithm for NuPRL type-theory is presented along with an over-view of the complications inherent in the use of this logic in automatic theorem provers.
Download:NO ONLINE COPY

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