The ILTP Problem Library for Intuitionistic Logic
Thomas Raths, Jens Otten, Christoph Kreitz.
Journal of Automated Reasoning, 38:261--271, 2007.
Abstract
	The Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem proving (ATP) systems for propositional and first-order intuitionistic logic. It includes about 2800 problems in a standardized syntax from 24 problem domains collected from various sources that are appropriate for intuitionistic logic. For each problem intuitionistic status and difficulty rating were obtained by running comprehensive tests of currently available intuitionistic ATP systems on all problems in the library. Thus for the first time the testing and evaluation of intuitionistic ATP systems is put onto a firm basis.

		(Preprint)	Back to overview of papers
Bibtex Entry
	@Article{ar:RathsOttenKreitz06a, author = "Thomas Raths and Jens Otten and Christoph Kreitz", title = "The ILTP Problem Library for Intuitionistic Logic", journal = "Journal of Automated Reasoning", year = 2007, volume = "38", number = "", pages = "261--271", }