• Pesca

  • Referenced in 164 articles [sw13664]
  • helps in the construction of proofs in sequent calculus. It works both as a proof ... classical and intuitionistic proposition and predicate calculi, and extend them by systems of nonlogical axioms...
  • CondLean

  • Referenced in 9 articles [sw09986]
  • their combinations. CondLean 3.0 implements sequent calculi for these logics. CondLean 3.0 improves CondLean...
  • NESCOND

  • Referenced in 5 articles [sw10041]
  • NESCOND: an implementation of nested sequent calculi for conditional logics. We present NESCOND, a theorem ... NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics CK and some...
  • Gen2sat

  • Referenced in 3 articles [sw16745]
  • deciding derivability in analytic pure sequent calculi. Gen2sat [1] is an efficient and generic tool ... classical logics given in terms of a sequent calculus. It contributes to the line ... reduction of derivability in analytic pure sequent calculi to SAT. This also makes Gen2sat ... assignment for teaching the concept of sequent calculi in a logic class for engineering practitioners...
  • JTabWb

  • Referenced in 2 articles [sw21865]
  • Java framework for implementing terminating sequent and tableau calculi. JTabWb is a Java framework ... developing provers based on sequent or tableau calculi. It provides a generic engine which searches...
  • tuCLEVER

  • Referenced in 1 article [sw41947]
  • then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode ... diamond formulas. Proof search using these calculi is terminating, and the completeness proof shows...
  • 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...
  • Ott

  • Referenced in 32 articles [sw00663]
  • Semantic definitions of full-scale programming languages are...
  • SETHEO

  • Referenced in 122 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • ML

  • Referenced in 524 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • CASL

  • Referenced in 174 articles [sw02235]
  • The specification language developed by CoFI is called...
  • OTTER

  • Referenced in 320 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • VAMPIRE

  • Referenced in 264 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • SQEMA

  • Referenced in 40 articles [sw03056]
  • Algorithmic correspondence and completeness in modal logic. IV...
  • Haskell

  • Referenced in 885 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • SPASS

  • Referenced in 185 articles [sw04108]
  • SPASS is an automated theorem prover for first...
  • HyTech

  • Referenced in 333 articles [sw04125]
  • HyTech is an automatic tool for the analysis...