Abstract
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.
Original language | American English |
---|---|
Journal | Default journal |
State | Published - Jan 1 1994 |
Keywords
- Theorem prover
- Meta-level architecture
- Resolution control strategies
- Design methodology
- Adequacy
Disciplines
- Business