|
|
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.
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
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
These are previous releases of the ILTP library. Please see
the documentation or the
history file for more details.
ILTP library v1.1.1
ILTP library v1.1.0
ILTP library v1.0
|