Home // COGNITIVE 2010, The Second International Conference on Advanced Cognitive Technologies and Applications // View article

A Tool for Experimenting with a Theorem Prover

Authors:
Foteini Grivokostopoulou
Ioannis Hatzilygeroudis

Keywords: Automated reasoning, Theorem prover, Resolution control strategies, TPTP library, Teaching logic assistant

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.

Pages: 78 to 83

Copyright: Copyright (c) IARIA, 2010

Publication date: November 21, 2010

Published in: conference

ISSN: 2308-4197

ISBN: 978-1-61208-108-3

Location: Lisbon, Portugal

Dates: from November 21, 2010 to November 26, 2010