Increasing the Versatility of Heuristic Based Theorem Provers
LPAR '93 Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning
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.