• ILTP

  • Referenced in 26 articles [sw00437]
  • Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... systems for first-order and propositional intuitionistic logic. It includes two problem collections for first ... about currently available ATP systems for intuitionistic logic and their performance results on the problems...
  • MiniML

  • Referenced in 46 articles [sw29625]
  • type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying...
  • leanCoP

  • Referenced in 24 articles [sw09756]
  • compact theorem prover for classical first-order logic, based on the connection (tableau) calculus ... compact theorem prover for intuitionistic first-order logic and based ... clausal connection calculus for intuitionistic logic. leanCoP 2.0 extends the classical prover leanCoP...
  • ileanCoP

  • Referenced in 15 articles [sw09757]
  • connection-based theorem proving in intuitionistic first-order logic. We present ... clausal connection calculus for first-order intuitionistic logic. It extends the classical connection calculus ... prefixes that encode the characteristics of intuitionistic logic. Our calculus is based on a clausal ... matrix characterisation for intuitionistic logic, which we prove correct and complete. The calculus was implemented...
  • Imogen

  • Referenced in 10 articles [sw11384]
  • Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. In this paper we describe Imogen ... theorem prover for intuitionistic propositional logic using the focused inverse method. We represent fine-grained...
  • Lilac

  • Referenced in 13 articles [sw08983]
  • take Abramsky’s term assignment for Intuitionistic Linear Logic (the linear term calculus...
  • STRIP

  • Referenced in 15 articles [sw04650]
  • system is a theorem prover for intuitionistic propositional logic with two main characteristics: it deals...
  • fCube

  • Referenced in 7 articles [sw11383]
  • fCube: an efficient prover for intuitionistic propositional logic. We present fCube, a theorem prover ... intuitionistic propositional logic based on a tableau calculus. The main novelty of fCube is that...
  • LMNtal

  • Referenced in 9 articles [sw07312]
  • simple logical interpretation based on intuitionistic linear logic and a flattening technique. This enables...
  • MetTeL

  • Referenced in 14 articles [sw11990]
  • prover for various modal, intuitionistic, hybrid, description and metric logics. The core component of MetTeL...
  • Teyjus

  • Referenced in 16 articles [sw21364]
  • prolog. The logic programming language λProlog is based on the intuitionistic theory of higher-order...
  • IntHistGC

  • Referenced in 3 articles [sw24227]
  • history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description ... theorem prover for intuitionistic propositional logic based on a sequent calculus with histories...
  • PITP

  • Referenced in 3 articles [sw11386]
  • PITP, a procedure to decide propositional intuitionistic logic, which turns out at the moment...
  • Minlog

  • Referenced in 2 articles [sw30424]
  • propositional minimal logic and Heyting’s intuitionist logic. It implements a decision procedure based...
  • intuit

  • Referenced in 4 articles [sw33643]
  • method for solving problems in intuitionistic propositional logic, which involves the use of an incremental...
  • SKIL

  • Referenced in 2 articles [sw25433]
  • with proofs. SKIL (synthesizing knowledge in intuitionistic logic) is an interactive theorem prover dedicated...
  • TILT

  • Referenced in 1 article [sw24052]
  • tableau-based theorem prover for intuitionistic logic). A tableau-based theorem prover for intuitionistic logic...
  • Lolliproc

  • Referenced in 5 articles [sw22624]
  • type systems based on the intuitionistic fragment of linear logic have been proposed, applications...
  • BDDIntKt

  • Referenced in 1 article [sw23446]
  • improved BDD method for intuitionistic propositional logic: BDDIntKt system description. We previously presented a decision ... satisfiability and validity in propositional intuitionistic logic Int using binary decision diagrams (BDDs...
  • Slakje

  • Referenced in 1 article [sw33644]
  • incomplete) automated theorem prover for intuitionistic logic. Our implementation of this prover approach, Slakje, performs ... competitively on the ILTP benchmark suite for intuitionistic provers: it solves...