The ILTP Library

Benchmarking Theorem Provers for Intuitionistic Logic


Welcome
Benchmark Problems
Provers and Results
Contact
 
Benchmark Problems

The ILTP library is divided into a first-order and a propositional part. All problems are represented in the standardized syntax of the TPTP library for classical logic. Both problem sets include some documentation, e.g. papers about the ILTP library, comparison tables, statistics files and a readme file. The tptp2X tool and some format files are included as well. They can be used for converting the problems into a syntax used by some of the existing intuitionistic ATP systems.

The following readme files give a brief introduction on how to use the ILTP library:

The performance results of some intuitionistic ATP systems on these benchmark problems can be found in the provers and results section. Previous releases of the ILTP library are made available in the archive section. Please contact us if you would like to submit new problems suitable for benchmarking intuitionistic ATP systems.


First-Order Part

The first-order part of the ILTP library contains 2550 problems including 70 propositional problems. 667 of these problems are known to be Theorems, 96 are Non-Theorems. The status of the remaining 1787 problems is Unsolved or Open. See the documentation for a detailed description.

ILTP library v1.1.2

Problem library: ILTP-v1.1.2-firstorder.tar.gz (gzipped, 1.8 Mbytes)
Statistics: ILTP-v1.1.2-fof-statistics.txt (97 kbytes)


Propositional Part

The propositional part of the ILTP library contains 274 propositional problems. 128 of these problems are known to be Theorems, 112 are Non-Theorems. The status of the remaining 34 problems is Unsolved or Open. See the documentation for a detailed description.

ILTP library v1.1.2

Problem library: ILTP-v1.1.2-propositional.tar.gz (gzipped, 767 kbytes)
Statistics: ILTP-v1.1.2-prop-statistics.txt (11 kbytes)


Archive

These are previous releases of the ILTP library. Please see the documentation or the history file for more details.

ILTP library v1.1.1

Problem files FOF: ILTP-v1.1.1-firstorder.tar.gz (gzipped, 1.8 Mbytes)
Statistics FOF: ILTP-v1.1.1-fof-statistics.txt (97 kbytes)
ATP system
comparison FOF:

ILTP-v1.1.1-fof-comparison.txt (176 kbytes)

Problem files prop: ILTP-v1.1.1-propositional.tar.gz (gzipped, 767 kbytes)
Statistics prop: ILTP-v1.1.1-prop-statistics.txt (11 kbytes)
ATP system
comparison prop:
ILTP-v1.1.1-prop-comparison.txt (19 kbytes)

ILTP library v1.1.0

Problem files FOF: ILTP-v1.1.0-firstorder.tar.gz (gzipped, 1.6 Mbytes)
Statistics FOF: ILTP-v1.1.0-fof-statistics.txt (97 kbytes)
ATP system
comparison FOF:

ILTP-v1.1.0-fof-comparison.txt (175 kbytes)

Problem files prop: ILTP-v1.1.0-propositional.tar.gz (gzipped, 572 kbytes)
Statistics prop: ILTP-v1.1.0-prop-statistics.txt (11 kbytes)
ATP system
comparison prop:
ILTP-v1.1.0-prop-comparison.txt (18 kbytes)

ILTP library v1.0

Problem files I: TPTP-v2.7.0-FOF.tar.gz (gzipped, 1.7 Mbytes)
Statistics I: TPTP-v2.7.0-FOF-statistics.txt (50 kbytes)

Problem files II: ILTP-set-v1.0.tar.gz (gzipped, 14 kbytes)
Statistics II: ILTP-set-v1.0-statistics.txt (5 kbytes)

ATP system
comparison:
ILTP-v1.0-comparison.txt (112 kbytes)


Jens Otten / Thomas Raths 01.03.2017