The ILTP Library

Benchmarking Theorem Provers for Intuitionistic Logic

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.