
Coq
 Referenced in 1818 articles
[sw00161]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... environment for semiinteractive development of machinechecked proofs. Typical applications include the formalization...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... Jersey ML. It implements various related type systems  the Edinburgh Logical Framework (LF), the Calculus ... powerful tool for interactive proof development in the natural deduction style. It supports refinement proof ... features of the system like argument synthesis and universe polymorphism make proof checking more practical...

Isar
 Referenced in 142 articles
[sw04599]
 Theorem proving system supporting both interactive proof development and some degree of automation have become ... semiautomated reasoning systems have an adequate primary notion of proof that is amenable ... broad range of automated proof methods. Interactive proof development is supported directly as well ... environment for live proof document editing. Thus proof texts may be developed incrementally by issuing...

Agda
 Referenced in 191 articles
[sw09689]
 development of your code). Agda is also a proof assistant: It is an interactive system ... proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed ... Löf. It has many similarities with other proof assistants based on dependent types, such...

UNITY
 Referenced in 185 articles
[sw13461]
 language and proof system defined by Chandy and Misra [5] for the development of parallel...

LCF
 Referenced in 157 articles
[sw08360]
 history. The original LCF system was a proofchecking program developed at Stanford University ... proof assistant for higher order logic originally developed for reasoning about hardware.2 The multifaceted ... contribution of Robin Milner to the development of HOL is remarkable. Not only ... underlying it and the innovative polymorphic type system used both...

Flyspeck
 Referenced in 113 articles
[sw10277]
 crosslinking formal and informal proof developments together. The platform supports writing natural language `narratives ... information at every proof step. We argue that such a system significantly lowers the threshold ... understanding formal development and facilitates collaboration on informal and formal parts of large developments...

E Theorem Prover
 Referenced in 192 articles
[sw10187]
 found, the system can provide a detailed list of proof steps that can be individually ... also provide possible answers (values for X). Development of E started as part ... release was in in 1998, and the system has been continuously improved ever since...

JProver
 Referenced in 13 articles
[sw09978]
 integration into the Nuprl proof development system...

OTTER
 Referenced in 315 articles
[sw02904]
 strategies for directing and restricting searches for proofs. Otter can also be used ... equational programming system. Otter is a fourthgeneration Argonne National Laboratory deduction system whose ancestors ... Note: Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. We recommend...

POOL
 Referenced in 14 articles
[sw03332]
 oriented language POOL. We develop a Hoarestyle proof system for partial correctness of programs...

SETHEO
 Referenced in 119 articles
[sw00707]
 programming language LOP (under development). The inference machine of the system is implemented using Prolog ... systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure...

LeoIII
 Referenced in 14 articles
[sw18516]
 developed. LeoIII combines its predecessor’s concept of cooperating external specialist systems with ... novel agentbased proof procedure. Key goals of the system’s development involve parallelism...

ETPS
 Referenced in 156 articles
[sw06302]
 promoting development of formal theories in a wide variety of disciplines, deductive information systems ... these disciplines, expert systems which can reason, and certain aspects of artificial intelligence ... facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction...

TAS
 Referenced in 11 articles
[sw04900]
 inference system This paper presents work on technology for transformational proof and program development ... theorems in the underlying logic. Our transformation system TAS compiles these rules to concrete deduction ... like drag&drop and proofbypointing, and a development management for transformational proofs...

Z/EVES
 Referenced in 43 articles
[sw10262]
 longer in development and has issues when used with modern operating systems. Z/EVES Eclipse brings ... supports all Z/EVES functionality: writing and sending proof commands to the prover, viewing proof output...

A3PAT
 Referenced in 8 articles
[sw21587]
 proofs. Software engineering, automated reasoning, rulebased programming or specifications often use rewriting systems ... ensured.This paper presents the approach developed in Project A3PAT to discover and moreover certify, with ... automation, termination proofs for term rewriting systems. It consists of two developments: the Coccinelle library ... techniques and termination criteria for the Coq proof assistant; the CiME3 rewriting tool translates termination...

INTOPT_90
 Referenced in 304 articles
[sw04705]
 results and ones that need further development. Algorithmic and practical tools are emphasized, theoretical considerations ... solution intervals. The chapter about solving nonlinear systems of equations (23 pages) features a rather ... John conditions and computationally executed proofs of the existence of feasible points generalizing Hansen...

HOLyHammer
 Referenced in 21 articles
[sw11553]
 upload and automatically process an arbitrary formal development (project) based on HOL Light ... reasoning systems combined with several premise selection methods trained on all the project proofs ... that contribute to its overall performance. The system is also available for local installation ... customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries...

TLA
 Referenced in 26 articles
[sw04442]
 proof system. All the tools are normally used from the Toolbox, an IDE (integrated development...