Show simple item record

dc.contributor.advisorMilner, Robin
dc.contributor.advisorBurstall, Rod
dc.contributor.advisorMeltzer, Bernard
dc.contributor.authorAubin, Raymond
dc.date.accessioned2013-04-05T11:39:40Z
dc.date.available2013-04-05T11:39:40Z
dc.date.issued1976
dc.identifier.urihttp://hdl.handle.net/1842/6649
dc.description.abstractThis 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_US
dc.contributor.sponsorCommonwealth Scholarship Commissionen_US
dc.contributor.sponsorConseil national de recherches du Canadaen_US
dc.language.isoenen_US
dc.publisherThe University of Edinburghen_US
dc.relation.hasversionAubin, 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_US
dc.subjectProof theoryen_US
dc.subjectAutomatic theorem provingen_US
dc.subjectInduction (Mathematics)en_US
dc.titleMechanizing Structural Inductionen_US
dc.typeThesis or Dissertationen_US
dc.type.qualificationlevelDoctoralen_US
dc.type.qualificationnamePhD Doctor of Philosophyen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record