Increasing the Versatility of Heuristic Based Theorem Provers

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.