Show simple item record

dc.contributor.advisorFleuriot, Jacques
dc.contributor.authorDixon, Lucas
dc.date.accessioned2006-06-16T16:57:33Z
dc.date.available2006-06-16T16:57:33Z
dc.date.issued2006-06
dc.identifier.urihttp://hdl.handle.net/1842/1250
dc.descriptionCentre for Intelligent Systems and their Applications
dc.description.abstractProof planning is a paradigm for the automation of proof that focuses on encoding intelligence to guide the proof process. The idea is to capture common patterns of reasoning which can be used to derive abstract descriptions of proofs known as proof plans. These can then be executed to provide fully formal proofs. This thesis concerns the development and analysis of a novel approach to proof planning that focuses on an explicit representation of choices during search. We embody our approach as a proof planner for the generic proof assistant Isabelle and use the Isar language, which is human-readable and machine-checkable, to represent proof plans. Within this framework we develop an inductive theorem prover as a case study of our approach to proof planning. Our prover uses the difference reduction heuristic known as rippling to automate the step cases of the inductive proofs. The development of a flexible approach to rippling that supports its various modifications and extensions is the second major focus of this thesis. Here, our inductive theorem prover provides a context in which to evaluate rippling experimentally. This work results in an efficient and powerful inductive theorem prover for Isabelle as well as proposals for further improving the efficiency of rippling. We also draw observations in order to direct further work on proof planning. Overall, we aim to make it easier for mathematical techniques, and those specific to mechanical theorem proving, to be encoded and applied to problems.en
dc.format.extent1350766 bytes
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.subject.otherPhD thesisen
dc.subject.otherProof planningen
dc.titleA Proof Planning Framework For Isabelleen
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