First-order 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-firstorder.tar.gz
> tar -xzf ILTP-v1.1.2-firstorder.tar.gz
This will create the directory ILTP-v1.1.2-firstorder.
Contents
--------
* Problems - benchmark formulas in a standardised syntax
* Axioms - axiom sets needed for formulating the problems
* tptp2X - tool for converting the formula into some of the existing
intuitionistic ATP system format
* Documents - performance results on the benchark formulas for some
intuitionistic ATP systems, statistics, example sessions,
readme-ILTP-v1.1.2-fof.txt - this file
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-firstorder/TPTP2X
> ./tptp2X_install
This 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 system. one of
ft, ftprolog, jprover, strip, ljt, pitp,
leancop (for the ATP-systems ileanCoP, ileanTAP, ileanSeP),
: one of AGT,ALG,COM,CSN,CSR,GEJ,GEO,GPJ,GRA,GRP,HAL,KRS,
LCL,MGT,MSC,NLP,NUM,PLA,PUZ,SET,SWC SWV,SYJ,SYN,TOP
: the most important ones are:
stdfof: transforms non-standard connectives like <=, <~>, ~|, ~&
into standard ones
shorten: replace symbols by short ones, suppress header information
add_equality: add equality axioms (necessary, if the prover has no
special method for handling equality) (*)
combination possible, e.g. -t stdfof+shorten+add_equality
Example: TPTP2X/tptp2X -f ft -t stdfof+shorten+add_equality
(*) add_equality is not completely stable under SWI-Prolog. If you work with
SWI-Prolog, please use also "shorten" (e.g. "-t shorten+add_equality"),
and replace write/1 by print/1 in the format-files.
For the ATP-system JProver:
The formulas for JProver must not contain Prolog-comments (starting
with %). So you may just copy tptp2X.main.no_comments to tptp2X.main.
Problems
--------
2550 problems of 24 domains
2480 non-propositional. 70 propositional
statistics: 2363 abstract problems, of which 20 are generic
class. status: 1950 valid, 553 invalid, 47 unknown
185 pure-equality problems
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