Mechanizing structural induction
This thesis proposes improved methods for the automatic generation of proofs by structural induction in a formal system. The main application considered is proving properties of programs. The theorem-proving problem divides into two parts: (1) a formal system, and (2) proof generating methods. A for...
Main Author: | |
---|---|
Other Authors: | |
Published: |
University of Edinburgh
1976
|
Subjects: | |
Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.253736 |
id |
ndltd-bl.uk-oai-ethos.bl.uk-253736 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-bl.uk-oai-ethos.bl.uk-2537362015-03-19T05:23:44ZMechanizing structural inductionAubin, RaymondMilner, Robin : Burstall, Rod : Meltzer, Bernard1976This thesis proposes improved methods for the automatic generation of proofs by structural induction in a formal system. The main application considered is proving properties of programs. The theorem-proving problem divides into two parts: (1) a formal system, and (2) proof generating methods. A formal system is presented which allows for a typed language; thus, abstract data types can be naturally defined in it. Its main feature is a general structural induction rule using a lexicographic ordering based on the substructure ordering induced by type definitions. The proof generating system is carefully introduced in order to convince of its consistency. It is meant to bring solutions to three problems. Firstly, it offers a method for generalizing only certain occurrences of a term in a theorem; this is achieved by associating generalization with the selection of induction variables. Secondly, it treats another generalization problem: that of terms occurring in the positions of arguments which vary within function definitions, besides recursion controlling arguments. The method is called indirect generalization, since it uses specialization as a means of attaining generalization. Thirdly, it presents a sound strategy for using the general induction rule which takes into account all induction subgoals, and for each of them, all induction hypotheses. Only then are the hypotheses retained and instantiated, or rejected altogether, according to their potential usefulness. The system also includes a search mechanism for counter-examples to conjectures, and a fast simplification algorithm.005Proof theory : Automatic theorem proving : Induction (Mathematics)University of Edinburghhttp://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.253736http://hdl.handle.net/1842/6649Electronic Thesis or Dissertation |
collection |
NDLTD |
sources |
NDLTD |
topic |
005 Proof theory : Automatic theorem proving : Induction (Mathematics) |
spellingShingle |
005 Proof theory : Automatic theorem proving : Induction (Mathematics) Aubin, Raymond Mechanizing structural induction |
description |
This thesis proposes improved methods for the automatic generation of proofs by structural induction in a formal system. The main application considered is proving properties of programs. The theorem-proving problem divides into two parts: (1) a formal system, and (2) proof generating methods. A formal system is presented which allows for a typed language; thus, abstract data types can be naturally defined in it. Its main feature is a general structural induction rule using a lexicographic ordering based on the substructure ordering induced by type definitions. The proof generating system is carefully introduced in order to convince of its consistency. It is meant to bring solutions to three problems. Firstly, it offers a method for generalizing only certain occurrences of a term in a theorem; this is achieved by associating generalization with the selection of induction variables. Secondly, it treats another generalization problem: that of terms occurring in the positions of arguments which vary within function definitions, besides recursion controlling arguments. The method is called indirect generalization, since it uses specialization as a means of attaining generalization. Thirdly, it presents a sound strategy for using the general induction rule which takes into account all induction subgoals, and for each of them, all induction hypotheses. Only then are the hypotheses retained and instantiated, or rejected altogether, according to their potential usefulness. The system also includes a search mechanism for counter-examples to conjectures, and a fast simplification algorithm. |
author2 |
Milner, Robin : Burstall, Rod : Meltzer, Bernard |
author_facet |
Milner, Robin : Burstall, Rod : Meltzer, Bernard Aubin, Raymond |
author |
Aubin, Raymond |
author_sort |
Aubin, Raymond |
title |
Mechanizing structural induction |
title_short |
Mechanizing structural induction |
title_full |
Mechanizing structural induction |
title_fullStr |
Mechanizing structural induction |
title_full_unstemmed |
Mechanizing structural induction |
title_sort |
mechanizing structural induction |
publisher |
University of Edinburgh |
publishDate |
1976 |
url |
http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.253736 |
work_keys_str_mv |
AT aubinraymond mechanizingstructuralinduction |
_version_ |
1716741295620227072 |