A Tool for Experimenting with a Theorem Prover
Foteini Grivokostopoulou, Ioannis Hatzilygeroudis · 2010
Abstract—In this paper, we presented EX-ACT-P, a tool for experimenting with a theorem prover. The heart of EX-ACT-P is ACT-P (A Configurable Theorem-Prover). ACT-P is a resolution-based theorem prover, which has a unique characteristic: allows the user to configure its resolution control regime. EX-ACT-P is an extension of ACT-P that allows user to experiment with theorem proving aspects, such as: configure a suitable resolution control regime, translate and automatically solve problems from the TPTP library, create and prove his/her own problems, display the proof steps in both text-based and graphical way and give information relevant to the proof process. So, EX-ACT-P can be useful to students for learning and to tutors for teaching aspects related to use of logic as a knowledge representation and reasoning language, by creating the right cognitive models, as well as to researchers for experimenting with theorem proving in ACT-P. A small scale evaluation for students has shown promising results.