Propositional part of the ILTP-v1.1.2-Library
---------------------------------------------
The Intuitionistic Logic Theorem Proving (ILTP) library provides a
platform for testing and benchmarking automated theorem proving
systems for first-order intuitionistic logic. It includes a collection
of propositional and first-order benchmark formulas in a standardised
syntax and tools for converting the formulas into some of the existing
intuitionistic theorem prover formats. It also includes information
about implementations of theorem provers for intuitionistic logic and
their perfomance results on the benchmark formulas.
Webpage: http://www.iltp.de.
Installation
------------
Unpack and untar ILTP-v1.1.2-propositional.tar.gz
> tar -xzf ILTP-v1.1.2-propositional.tar.gz
This will create the directory ILTP-v1.1.2-propositional.
Contents
--------
* Problems - benchmark formulas in a standardised syntax
* tptp2X - tool for converting the formula into some of the existing
intuitionistic ATP system format:
* Documents - formula and result statistics
tptp2X
------
This tool translates the problems into the syntax of the
Automatic-Theorem-Proving (ATP)-systems. It stems from the
TPTP-Library [1]. So-called format-files specify the syntax of the
respective ATP system.
You will need some Prolog Interpreter. For full details see the
technical manual at http://www.cs.miami.edu/~tptp.
a) Configure tptp2X tool:
> cd ILTP-v1.1.2-propositional/TPTP2X
> ./tptp2X_install
Thi s script will ask for required information. (When you are asked to
state your desired format, then simply type 'a' for 'all').
b) Use TPTP2X tool to translate formulas:
> cd ..
> TPTP2X/tptp2X -f [-t ] [Problems//'*.p']
This will write the translated formulas into the directory .
The parameters are:
: intuitionistic ATP systems are one of
ft, ftprolog, jprover, strip, ljt, pitp,
leancop (for ileanCoP, ileanTAP, ileanSeP),
: one of LCL,SYN,SYJ
: the most important ones are:
stdfof: transforms non-standard connectives like <=, <~>, ~|, ~&
into standard ones
shorten: replace symbols by short ones, suppess header information
combination possible, e.g. -t stdfof+shorten
Example: TPTP2X/tptp2X -f strip -t stdfof+shorten
Problems
--------
274 problems
statistics: 41 abstract problems, of which 15 are generic,
status: 139 intuit. valid, 134 class. but not intuit. valid, 1 class. invalid
References
----------
[1] G. Sutcliffe, C. Suttner. The TPTP problem library - CNF release
v1.2.1. Journal of Automated Reasoning, 21: 177-203, 1998.
http://www.cs.miami.edu/~tptp/
Contact
-------
Please contact us, if you have any questions, suggestions, or if you
have developed an ATP system or benchmark formulas for intuitionistic
logic. We would like to include your ATP system and your benchmark
formulas in the ILTP-library.
http://www.iltp.de
Thomas Raths
Jens Otten
University of Potsdam
Department of Computer Science
August-Bebel-Straße 89
14482 Potsdam
Germany