Theorem proving in undecidable theories has to resort to <I>semi-decision procedures</I>, 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 also be improved when the decidability of subclasses of formulae is explored. <I>Decision procedures </I>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. Evidence 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. (i) <I>juxtaposition</I>, where each component of the system operates independently from the others, and there is no communication between them, (ii) <I>cooperation</I>, where the behaviour of a component influences others, and communication is direct, and (iii) <I>interfacing</I>, where transformation or simplification steps take place before a formula is delivered to a component of the system, in which case communication amongst modules is mediated. From the decision procedure viewpoint, the main effect of its integration into a prover is the enlargement of the decidable domain, whereas, for the heuristic component, there is a reduction in the number of subproblems it has to address.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:642261 |
| Date | January 1995 |
| Creators | Busatto, Renato |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/21666 |
Page generated in 0.002 seconds