
ILTP
 Referenced in 26 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 26 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...

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

ileanCoP
 Referenced in 17 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...

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

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

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

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