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 26 articles )

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

1 2 next

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

1 2 next