Mechanizing structural induction
dc.contributor.advisor
Milner, Robin
en
dc.contributor.advisor
Burstall, Rod
en
dc.contributor.advisor
Meltzer, Bernard
en
dc.contributor.author
Aubin, Raymond
en
dc.contributor.sponsor
Commonwealth Scholarship Commission
en
dc.contributor.sponsor
Conseil national de recherches du Canada
en
dc.date.accessioned
2013-04-05T11:39:40Z
dc.date.available
2013-04-05T11:39:40Z
dc.date.issued
1976
dc.description.abstract
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.
en
dc.identifier.uri
http://hdl.handle.net/1842/6649
dc.language.iso
en
dc.publisher
The University of Edinburgh
en
dc.relation.hasversion
Aubin, Raymond. "Some generalization heuristics in proofs by induction." In Actes du collocue Construction, amelioration et verification de programmes, pp. 197-208. Edite par G. Huet et G. Kahn. Rocquencourt, France: Institut de recherche d'informatique et d'automatique, 1975.
en
dc.subject
Proof theory
en
dc.subject
Automatic theorem proving
en
dc.subject
Induction (Mathematics)
en
dc.title
Mechanizing structural induction
en
dc.type
Thesis or Dissertation
en
dc.type.qualificationlevel
Doctoral
en
dc.type.qualificationname
PhD Doctor of Philosophy
en
Files
Original bundle
1 - 1 of 1
- Name:
- Aubin1976.pdf
- Size:
- 1.53 MB
- Format:
- Adobe Portable Document Format
- Description:
This item appears in the following Collection(s)