ACT-P: A configurable theorem-prover

摘要

There has been a considerable amount of research into the provision of explicit representation of control regimes for resolution-based theorem provers. However, most of the existing systems are either not adequate or too inefficient to be of practical use. In this paper a theorem prover, ACT-P, which is adequate but retains satisfactory efficiency is presented. It does so by providing a number of user-changeable heuristics which are called at specific points during the search for a proof. The set of user-changeable heuristics was determined on the basis of a classification of the heuristics used by existing resolution-based theorem provers.