Abstract
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.
Original language | English |
---|---|
Title of host publication | LPAR '93 Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning |
Publisher | Springer |
Volume | Lecture Notes in Artificial Intelligence No. 698 |
ISBN (Print) | 3-540-56944-8 |
Publication status | Published - 1993 |