The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic

Jens Otten, Thomas Raths, Christoph Kreitz.

International Conference TABLEAUX-2005, LNAI 3702, pp. 333-337, Springer Verlag, 2005.


The Intuitionistic Logic Theorem Proving (ILTP) Library provides a platfom for testing and benchmarking theorem provers for first-order intuitionistic logic. It includes a collection of benchmark problems in a standardised syntax and performance results obtained by a comprehensive test of currently available intuitionistic theorem proving systems. These results are used to provide information about the status and the difficulty rating of the benchmark problems.

PS Version PDF Version   (Preprint) BACK
Back to overview of papers

Bibtex Entry

@InProceedings{inp:OttenRathsKreitz05a, author = "Jens Otten and Thomas Raths and Christoph Kreitz", title = "{The ILTP Library}: Benchmarking Automated Theorem Provers for Intuitionistic Logic", booktitle = "International Conference TABLEAUX-2005", year = 2005, editor = "Bernhard Beckert", series = "Lecture Notes in Artificial Intelligence", volume = 3702, pages = "333--337", publisher = "Springer Verlag" }