Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #92133 | |
|---|---|
| Title: | Representing Preference in Proof Plans |
| Authors: | Manning,AJ |
| Date: | 1992 |
| Presented: | |
| Keywords: | |
| Abstract: | The Mathematical Reasoning Group at Edinburgh University have developed the technique of proof plans, [Bundy et al 91], as part of their OYSTER-CLAM theorem proving system. This system develops the proof of a mathematical conjecture in two distinct phases, the first using a search strategy, constructs a feasible proof plan, the second applies it. Each of the search strategies available to the system is embedded in an individual planner, any one of which can be used to attempt the planning process. This project details how a new planner, which employs the best first search strategy, has been developed within the current system. The heuristic evaluation function, which forms the backbone of this new planner, was devised in parallel, and allows for the idea of preference to be incorporated directly into the planning process. This report gives some examples of where proof plans developed using this new planner show a marked improvement upon those devised by the other planners. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}