Title

ACT-P: A configurable theorem prover.

SelectedWorks Author Profiles:

Han Reichgelt

Document Type

Article

Publication Date

1994

Date Issued

January 1994

Date Available

July 2014

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.

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.

Language

en_US

Publisher

Elsevier

Creative Commons License

Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License.