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.

References in zbMATH (referenced in 29 articles )

Showing results 1 to 20 of 29.
Sorted by year (citations)

1 2 next

  1. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  2. Otten, Jens: The \textsfnanoCoP2.0 connection provers for classical, intuitionistic and modal logics (2021)
  3. Cassano, Valentin; Fervari, Raul; Hoffmann, Guillaume; Areces, Carlos; Castro, Pablo F.: A tableaux calculus for default intuitionistic logic (2019)
  4. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
  5. Ferrari, Mauro; Fiorentini, Camillo: Goal-oriented proof-search in natural deduction for intuitionistic propositional logic (2019)
  6. Fiorentini, Camillo; Goré, Rajeev; Graham-Lengrand, Stéphane: A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic (2019)
  7. Olarte, Carlos; de Paiva, Valeria; Pimentel, Elaine; Reis, Giselle: The ILLTP library for intuitionistic linear logic (2019)
  8. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: JTabWb: a Java framework for implementing terminating sequent and tableau calculi (2017)
  9. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
  10. Dyckhoff, Roy: Intuitionistic decision procedures since Gentzen (2016)
  11. Brock-Nannestad, Taus; Chaudhuri, Kaustuv: Disproving using the inverse method by iterative refinement of finite approximations (2015)
  12. Goré, Rajeev; Thomson, Jimmy; Wu, Jesse: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description (2014)
  13. Stump, Aaron; Sutcliffe, Geoff; Tinelli, Cesare: StarExec: a cross-community infrastructure for logic solving (2014) ioport
  14. Goré, Rajeev; Thomson, Jimmy: An improved BDD method for intuitionistic propositional logic: BDDIntKt system description (2013)
  15. Raths, Thomas; Otten, Jens: The QMLTP problem library for first-order modal logics (2012)
  16. Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido: fCube: an efficient prover for intuitionistic propositional logic (2010)
  17. Fiorino, Guido: Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus (2010)
  18. Otten, Jens: Restricting backtracking in connection calculi (2010)
  19. Sutcliffe, Geoff; Benzmüller, Christoph: Automated reasoning in higher-order logic using the TPTP THF infrastructure (2010)
  20. Burel, Guillaume: Automating theories in intuitionistic logic (2009)

1 2 next