Division of Informatics
Forrest Hill & 80 South Bridge
PhD Thesis #9504 | |
|---|---|
| Title: | The Use of Proof Planning in Normalisation |
| Authors: | Busatto-Neto,R |
| Date: | 1995 |
| Presented: | |
| Keywords: | |
| Abstract: | Theorem proving in undecidable theories has to resort to semi-decision procedures, i.e. partial computable functions that halt when the input formula is a theorem, but may not terminate otherwise. Their performance can be improved once heuristic mechanisms are introduced to guide search. Heuristic functions, however, sometimes assume the properties of a particular subclass of formulae to be valid in a larger domain, and may as a result fail to recognise a theorem due to the loss of completeness.Efficiency may be also improved when the decidability of subclasses of formulae is explored. Decision procedures establish, after a finite amount of time and computation, whether a formula of a class is a theorem or not. Their main advantage is their total computability, i.e. computation terminates for every formula of the domain, whether it is a theorem or not. Their reduced scope of application and, in some cases, their complexity are, nonetheless, the main limitations.Evindence suggests that the development of efficient mechanical theorem provers requires the integration of both heuristic modules and decision procedures inside hybrid systems. Integration is achieved through at least three strategies ..... |
| 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}