• ILTP

  • Referenced in 28 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...
  • leanCoP

  • Referenced in 31 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 18 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...
  • MiniML

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

  • Referenced in 11 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 14 articles [sw08983]
  • take Abramsky’s term assignment for Intuitionistic Linear Logic (the linear term calculus...
  • fCube

  • Referenced in 9 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...
  • STRIP

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

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

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

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

  • Referenced in 2 articles [sw40829]
  • ILLTP library for intuitionistic linear logic. Benchmarking automated theorem proving (ATP) systems using standardized problem ... library for benchmarking Girard’s (propositional) intuitionistic linear logic. For a quick bootstrapping ... linear logic theorems, we use translations of the collection of Kleene’s intuitionistic theorems ... analyze four different translations of intuitionistic logic into linear logic and compare their proofs using...
  • 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...