The ILTP Problem Library for Intuitionistic Logic


Thomas Raths, Jens Otten, Christoph Kreitz.  
Journal of Automated Reasoning, 38:261271, 2007. 

Abstract 

The Intuitionistic Logic Theorem Proving (ILTP) library provides a
platform for testing and benchmarking automated theorem proving (ATP)
systems for propositional and firstorder 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 = "261271", } 