The use of proof planning in normalisation
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...
| Main Author: | |
|---|---|
| Published: |
University of Edinburgh
1995
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.642261 |