Increasing the Versatility of Heuristic Based Theorem Provers
LPAR '93 Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning
MetadataShow full item record
Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety of specific instances where the fixed ordering breaks down. We present an approach liberates such systems by introducing a more versatile framework for organising proof strategies.