• Pesca

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

  • Referenced in 48 articles [sw03709]
  • natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which ... free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically...
  • MUltlog

  • Referenced in 19 articles [sw06604]
  • MUltlog is a system which takes as input the specification of a finitely-valued first ... logic and produces a sequent calculus, a natural deduction system, and clause formation rules...
  • CERES

  • Referenced in 21 articles [sw09442]
  • CERES system with special emphasis on the extraction of Herbrand sequents and simplification methods...
  • Tac

  • Referenced in 7 articles [sw09455]
  • searching for sequent calculus proofs. We present a focused proof system for a first-order...
  • Abella

  • Referenced in 52 articles [sw09461]
  • System Description). Abella [3] is an interactive system for reasoning about aspects of object languages ... calculus, cut admissibility for a sequent calculus and type uniqueness and subject reduction properties. This...
  • Bedwyr

  • Referenced in 23 articles [sw09460]
  • syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation ... finite failure can be captured in the sequent calculus by incorporating inference rules for definitions...
  • JProver

  • Referenced in 13 articles [sw09978]
  • first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve ... integration into the Nuprl proof development system...
  • Minlog

  • Referenced in 2 articles [sw30424]
  • free sequent calculus formulation of these systems. While the method it uses is rather unsophisticated...
  • IntHistGC

  • Referenced in 3 articles [sw24227]
  • intuitionistic propositional logic using global caching: IntHistGC system description. We describe an implementation ... intuitionistic propositional logic based on a sequent calculus with histories due to Corsi and Tassi...
  • PAT

  • Referenced in 3 articles [sw34502]
  • micro- and macrotasking, IBM Parallel Fortran, and Sequent Parallel Fortran constructs for parallelism ... been ported to a range of Unix systems, using X-windows for their graphics interface...
  • ILLTP

  • Referenced in 3 articles [sw40829]
  • linear logic. Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well ... encode such problems as linear logic sequents, thus enlarging our collection of problems...
  • SDTrimSP

  • Referenced in 3 articles [sw27040]
  • code SDTrimSP (Static and Dynamic Trim for Sequental and Parallel computer) was developed. SDTrimSP ... machines, IBM Power4 and Power5 systems, Cray T3E, NEC SX5, and Linux clusters with...
  • Filaments

  • Referenced in 5 articles [sw04841]
  • machines. It currently runs on an SGI, Sequent, and a cluster of Sun IPCs. Prototypes ... complexity into a run-time system. To this end, we have validated Filaments by creating...
  • WorkflowFM

  • Referenced in 1 article [sw21519]
  • composition. We present a logic-based system for process specification and composition named WorkflowFM ... specification of abstract processes as logical sequents and their composition via formal proof. The result ... multiple concurrent users to interact with the system through a purely diagrammatic interface, while...
  • GenTreeCad

  • Referenced in 1 article [sw33688]
  • logic using point-plus-expressions. The LATEX system is widely used in scientific journals with ... construct numerous derivations using Gentzen-style sequent calculus, gives the idea to automatize the process...
  • tuCLEVER

  • Referenced in 1 article [sw41947]
  • strongest logics in Lewis’ family of conditional systems, characterized by uniformity and total reflexivity ... then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode...
  • kTAM

  • Referenced in 1 article [sw22257]
  • algorithmic design of DNA self-assembly systems. It employs the use of so-called ... implementations of DNA tiles and their sub-sequent algorithmic assembly into larger complexes ... only for a few types of these systems. This might be due to the fact...
  • ADOL-C

  • Referenced in 257 articles [sw00019]
  • ADOL-C: Automatic Differentiation of C/C++. We present...
  • Coq

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