Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #93126 | |
|---|---|
| Title: | The Use of Abduction to Correct Faulty Conjectures |
| Authors: | Monroy-Borja,R |
| Date: | 1993 |
| Presented: | |
| Keywords: | |
| Abstract: | Theorem proving is the systematic derivation of a mathematical proof from a set of axioms by the use of rules of inference. The problem of building an artificial mathematician to automate this process has been studied since the first hesitant steps taken by a young science called Artificial Intelligence, AI. We are interested in a related but far less explored problem: the analyses and correction of false conjectures, especially where that correction involves finding a collection of antecedents that, together with a set of axioms, transform non-theorems into theorems. Reasoning and searching are necessary for the solution to this problem. Abduction seems to be a candidate mechanism for the former. However, most failed proof search spaces are huge, and especial care is to be taken in order to tackle the combinatorial explosion phenomenon which may make intractable the latter. Fortunately, the planing search space generated by proof plans are an exception [Bundy 88] - they are moderately small. Furthermore, the meta-level reasoning used to guide the plan formation provides us with a basis for analysing the failure and the partial success derived from a proof attempt. We have explored the possibility of using the proof plans technique to implement an abduction mechanism for correcting faulty conjectures. The results that were obtained throughout our experiments are reported in this dissertation. |
| 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}