|
|
Welcome to the ILTP Library
|
The Intuitionistic Logic Theorem Proving (ILTP) library provides
a platform for testing and benchmarking
automated theorem proving (ATP) systems for first-order and
propositional intuitionistic logic.
It includes two problem collections
for first-order and propositional intuitionistic ATP systems
and tools for converting the problems into the input syntax of
some existing intuitionistic ATP systems. It also includes
information about currently available
ATP systems for intuitionistic logic and their performance
results on the problems in the ILTP library.
Please contact
us for further information or if you want to submit new benchmark
problems or performance results.
Features of the ILTP Library:
-
About 2800 propositional and first-order benchmark problems in a
standardized syntax.
-
Information about the intuitionistic status of all benchmark
problems, i.e. Theorem, Non-Theorem, Unknown or Open.
-
Information about the intuitionistic rating of the benchmark
problems, i.e. the relative difficulty of the problems with
respect to current state-of-the-art systems.
-
Tools for translating the benchmark problems into a syntax
of some existing intuitionistic ATP systems.
-
Information about currently available ATP systems for
intuitionistic logic and their performance on all
problems in the ILTP library.
The ILTP library is suitable for developing, testing and evaluating
novel calculi, search strategies and ATP implementations for
intuitionistic logic.
The draft of the journal article describes the current version of the
ILTP library:
-
Thomas Raths, Jens Otten, Christoph Kreitz.
The ILTP Problem Library for Intuitionistic Logic -
Release v1.1.
Journal of Automated Reasoning.
©
Kluwer, 2006.
·
iltp_jar06.pdf (195 kbytes)
·
iltp_jar06.dvi (43 kbytes)
The following paper gives a short description of the ILTP library v1.0:
-
Thomas Raths, Jens Otten, Christoph Kreitz.
The ILTP Library: Benchmarking Theorem Provers for
Intuitionistic Logic.
In B. Beckert, editor, Automated Reasoning with Analytic Tableaux
and Related Methods, TABLEAUX 2005, LNAI 3702, pages 333-337.
©
Springer Verlag, 2005.
·
iltp_tab05.pdf (124 kbytes)
·
iltp_tab05.dvi (23 kbytes)
Please contact us if you have any question about the ILTP library.
If you have developed an automated theorem proving system
for intuitionistic logic please let us know about it. We would like
to include information about your system and its performance
on this site. If you have created new propositional or
first-order problems suitable for testing and benchmarking
intuitionistic ATP systems, we would like to include them in
the ILTP library. If these problems are of interest for
testing and benchmarking classical theorem provers as well, we would
suggest to submit them to the
TPTP library in order
to make them available to people involved in developing ATP systems
for classical logic as well.
|