• KRIPKE

  • Referenced in 8 articles [sw01162]
  • appropriate vocabulary) the decision procedure for each of these logics describes a way of recursively ... proof-search which will contain as a sub-tree 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 proof-search 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 sat-modulo...
  • 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, general-purpose purely functional...
  • STRIP

  • Referenced in 15 articles [sw04650]
  • STRIP: Structural sharing for efficient proof-search. The...
  • HOL

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

  • Referenced in 700 articles [sw06233]
  • Maude is a high-performance reflective language and...
  • Nuprl

  • Referenced in 396 articles [sw06751]
  • The Nuprl system is a framework for reasoning...
  • 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 history-based theorem prover for intuitionistic propositional...
  • 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...