
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 ... freevariable 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 finitelyvalued 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 firstorder...

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]
 firstorder intuitionistic theorem prover that creates sequentstyle 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 Xwindows 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 runtime system. To this end, we have validated Filaments by creating...

WorkflowFM
 Referenced in 1 article
[sw21519]
 composition. We present a logicbased 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 pointplusexpressions. The LATEX system is widely used in scientific journals with ... construct numerous derivations using Gentzenstyle 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 selfassembly systems. It employs the use of socalled ... implementations of DNA tiles and their subsequent algorithmic assembly into larger complexes ... only for a few types of these systems. This might be due to the fact...

ADOLC
 Referenced in 257 articles
[sw00019]
 ADOLC: Automatic Differentiation of C/C++. We present...

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