ACT-P: A configurable theorem prover.

Ioannis Hatzilygeroudis, Han Reichgelt, Johannes (Han) Reichgelt

Research output: Contribution to journalArticlepeer-review

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 languageAmerican English
JournalDefault journal
StatePublished - Jan 1 1994

Keywords

  • Theorem prover
  • Meta-level architecture
  • Resolution control strategies
  • Design methodology
  • Adequacy

Disciplines

  • Business

Cite this