Show simple item record

dc.contributor.advisorBundy, Alan
dc.contributor.advisorGreen, Ian
dc.contributor.advisorFleuriot, Jacques
dc.contributor.authorGow, Jeremy
dc.date.accessioned2004-12-21T13:44:03Z
dc.date.available2004-12-21T13:44:03Z
dc.date.issued2004-07
dc.identifier.urihttp://hdl.handle.net/1842/643
dc.descriptionCentre for Intelligent Systems and their Applications
dc.description.abstractA key problem in automating proof by mathematical induction is choosing an induction rule suitable for a given conjecture. Since Boyer & Moore’s NQTHM system the standard approach has been based on recursion analysis, which uses a combination of induction rules based on the relevant recursive function definitions. However, there are practical examples on which such techniques are known to fail. Recent research has tried to improve automation by delaying the choice of inductive rule until later in the proof, but these techniques suffer from two serious problems. Firstly, a lack of search control: specifically, in controlling the application of ‘speculative’ proof steps that partially commit to a choice of induction rule. Secondly, a lack of generality: they place significant restrictions on the form of induction rule that can be chosen. In this thesis we describe a new delayed commitment strategy for inductive proof that addresses these problems. The strategy dynamically creates an appropriate induction rule by proving schematic proof goals, where unknown rule structure is represented by meta-variables which become instantiated during the proof. This is accompanied by a proof that the generated rule is valid. The strategy achieves improved control over speculative proof steps via a novel speculation critic. It also generates a wider range of useful induction rules than other delayed commitment techniques, partly because it removes unnecessary restrictions on the individual proof cases, and partly because of a new technique for generating the rule’s overall case structure. The basic version of the strategy has been implemented using the lamdaClam proof planner. The system was extended with a novel proof critics architecture for this purpose. An evaluation shows the strategy is a useful and practical technique, and demonstrates its advantages.en
dc.format.extent1426674 bytes
dc.format.extent1267352 bytes
dc.format.mimetypeapplication/postscript
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.subject.otherInduction Rulesen
dc.subject.otherProof Planningen
dc.titleThe Dynamic Creation of Induction Rules Using Proof Planningen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record