
ILTP
 Referenced in 28 articles
[sw00437]
 Intuitionistic Logic Theorem Proving (ILTP) library provides a platform for testing and benchmarking automated theorem ... systems for firstorder 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 firstorder logic, based on the connection (tableau) calculus ... compact theorem prover for intuitionistic firstorder logic and based ... clausal connection calculus for intuitionistic logic. leanCoP 2.0 extends the classical prover leanCoP...

ileanCoP
 Referenced in 18 articles
[sw09757]
 connectionbased theorem proving in intuitionistic firstorder logic. We present ... clausal connection calculus for firstorder 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 finegrained...

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 higherorder...

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]
 historybased 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]
 tableaubased theorem prover for intuitionistic logic). A tableaubased 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...