
KRIPKE
 Referenced in 8 articles
[sw01162]
 appropriate vocabulary) the decision procedure for each of these logics describes a way of recursively ... proofsearch which will contain as a subtree a proof of A if there ... nite. However in practice this decision procedure tends to be impossible...

Psyche
 Referenced in 5 articles
[sw28518]
 style architecture. Psyche is a modular proofsearch engine designed for either interactive or automated ... correctness but also the completeness of proof search. It addresses the second by offering ... Psyche features the ability to call decision procedures such as those used in satmodulo...

Coq
 Referenced in 1906 articles
[sw00161]
 Coq is a formal proof management system. It...

ILTP
 Referenced in 29 articles
[sw00437]
 The Intuitionistic Logic Theorem Proving (ILTP) library provides...

Isabelle
 Referenced in 719 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

PVS
 Referenced in 634 articles
[sw03484]
 PVS is a verification system: that is, a...

Haskell
 Referenced in 885 articles
[sw03521]
 Haskell is a standardized, generalpurpose purely functional...

STRIP
 Referenced in 15 articles
[sw04650]
 STRIP: Structural sharing for efficient proofsearch. The...

HOL
 Referenced in 594 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

Maude
 Referenced in 700 articles
[sw06233]
 Maude is a highperformance reflective language and...

Nuprl
 Referenced in 396 articles
[sw06751]
 The Nuprl system is a framework for reasoning...

Automath
 Referenced in 414 articles
[sw07127]
 Automath is a language designed by N.G. the...

LEGO
 Referenced in 108 articles
[sw09685]
 LEGO is an interactive proof development system (proof...

fCube
 Referenced in 9 articles
[sw11383]
 fCube: an efficient prover for intuitionistic propositional logic...

Imogen
 Referenced in 11 articles
[sw11384]
 Imogen: Focusing the Polarized Inverse Method for Intuitionistic...

JTabWb
 Referenced in 2 articles
[sw21865]
 JTabWb: a Java framework for implementing terminating sequent...

IntHistGC
 Referenced in 3 articles
[sw24227]
 A historybased theorem prover for intuitionistic propositional...

Cambridge LCF
 Referenced in 27 articles
[sw31981]
 Logic and computation. Interactive proof with Cambridge LCF...

intuit
 Referenced in 4 articles
[sw33643]
 SAT modulo intuitionistic implications. We present a new...

Lolli
 Referenced in 52 articles
[sw40831]
 Lolli is a logic programming language based on...