USF St. Petersburg campus Faculty Publications
ACT-P: A configurable theorem prover.
Document Type
Article
Publication Date
1994
ISSN
0169-023X
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.
Language
en_US
Publisher
Elsevier
Recommended Citation
Hatzilygeroudis, I., Reichgelt, H. (1994). ACT-P: A configurable theorem prover. Data & Knowledge Engineering, 12, 277-296. doi: 10.1016/0169-023X(94)90029-9
Creative Commons License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License.
Comments
Citation only. Full-text article is available through licensed access provided by the publisher. Published in Data & Knowledge Engineering, 12, 277-296. doi: 10.1016/0169-023X(94)90029-9. Members of the USF System may access the full-text of the article through the authenticated link provided.