
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 freevariable 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]
 firstorder logic and produces a sequent calculus, a natural deduction system, and clause formation...

Psyche
 Referenced in 5 articles
[sw28518]
 proofsearch engine based on sequent calculus with an LCFstyle 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 cutfree 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): DEAKcalculustool, Sequentcalculustool...

GenTreeCad
 Referenced in 1 article
[sw33688]
 construct numerous derivations using Gentzenstyle 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]
 firstorder 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 higherorder syntax in...

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