• Pesca

  • Referenced in 129 articles [sw13664]
  • PESCA = Proof Editor for Sequent Calculus: Pesca is a program that helps in the construction ... proofs in sequent calculus. It works both as a proof editor and as an automatic...
  • leanTAP

  • Referenced in 38 articles [sw09985]
  • implementation of a sequent calculus. He shows correctness and completeness of this calculus. Since ... correspondence between the sequent calculus and the program leanTAP is evident, this in turn constitutes ... leanTAP. Next, the author generalizes the sequent calculus to the modal logic K and sketches ... proof of the completeness of this sequent calculus. Then, the author transforms the sequent calculus...
  • Abella

  • Referenced in 49 articles [sw09461]
  • calculus, cut admissibility for a sequent calculus and type uniqueness and subject reduction properties. This...
  • KeYmaera

  • Referenced in 39 articles [sw03709]
  • KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose...
  • Bedwyr

  • Referenced in 21 articles [sw09460]
  • failure can be captured in the sequent calculus by incorporating inference rules for definitions that ... result, proof search in such a sequent calculus can capture simple model checking problems...
  • Cyclist

  • Referenced in 20 articles [sw18519]
  • cyclic theorem provers based on a sequent calculus. In addition, over the years several decision...
  • MUltlog

  • Referenced in 17 articles [sw06604]
  • first-order logic and produces a sequent calculus, a natural deduction system, and clause formation...
  • Psyche

  • Referenced in 5 articles [sw28518]
  • proof-search engine based on sequent calculus with an LCF-style architecture. Psyche ... deduction: it uses instead a focused sequent calculus for polarised classical logic. Finally, Psyche features...
  • Tac

  • Referenced in 7 articles [sw09455]
  • determinism involved in searching for sequent calculus proofs. We present a focused proof system...
  • Aglet

  • Referenced in 4 articles [sw13305]
  • search procedure, based on a focused sequent calculus, to ease the burden of constructing proofs...
  • AgsyHOL

  • Referenced in 4 articles [sw13302]
  • Proof terms are a kind of sequent calculus derivations and are so far only printed...
  • Gen2sat

  • Referenced in 3 articles [sw16745]
  • logics given in terms of a sequent calculus. It contributes to the line of research ... reduction of derivability in analytic pure sequent calculi to SAT. This also makes Gen2sat...
  • IntHistGC

  • Referenced in 3 articles [sw24227]
  • intuitionistic propositional logic based on a sequent calculus with histories due to Corsi and Tassi...
  • Minlog

  • Referenced in 2 articles [sw30424]
  • procedure based on a cut-free sequent calculus formulation of these systems. While the method...
  • DEAK calculus

  • Referenced in 1 article [sw28673]
  • version of an LK Sequent calculus fragment are available as Scala JAR files (these have ... Linux and macOS): DEAK-calculus-tool, Sequent-calculus-tool...
  • GenTreeCad

  • Referenced in 1 article [sw33688]
  • construct numerous derivations using Gentzen-style sequent calculus, gives the idea to automatize the process ... dual, and then the connection between sequent calculus and the tableau method...
  • Logitext

  • Referenced in 1 article [sw32232]
  • first-order classical logic using the sequent calculus, in the same tradition as Jape, Pandora...
  • Coq

  • Referenced in 1784 articles [sw00161]
  • Coq is a formal proof management system. It...
  • HYBRID

  • Referenced in 18 articles [sw00421]
  • Hybrid: a package for higher-order syntax in...
  • ILTP

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