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

UNITY
 Referenced in 173 articles
[sw13461]
 computational model, specification language and proof system defined by Chandy and Misra...

LEGO
 Referenced in 106 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 ... style. It supports refinement proof as a basic operation. The system design emphasizes removing ... tedious aspects of interactive proofs. For example, features of the system like argument synthesis...

Isar
 Referenced in 138 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 ... well. The Isabelle system offers Isar as an alternative proof language interface layer, beyond traditional ... scripts. The Isabelle/Isar system provides an interpreter for the Isar formal proof document language. Isabelle/Isar...

OBJ3
 Referenced in 138 articles
[sw05370]
 OBJ3 is a program specification and proof system based on order sorted equational logic...

Twelf
 Referenced in 167 articles
[sw06888]
 specify, implement, and prove properties of deductive systems such as programming languages and logics. Large ... typed assembly language, a foundational proofcarryingcode system, and a type safety proof...

E Theorem Prover
 Referenced in 183 articles
[sw10187]
 order form. The system will then try to find a formal proof for the conjecture ... assuming the axioms. If a proof is found, the system can provide a detailed list ... proof steps that can be individually verified. If the conjecture is existential ... release was in in 1998, and the system has been continuously improved ever since...

Agda
 Referenced in 173 articles
[sw09689]
 interactive system for writing and checking proofs. Agda is based on intuitionistic type theory ... foundational system for constructive mathematics developed by the Swedish logician Per MartinLöf ... many similarities with other proof assistants based on dependent types, such as Coq, Epigram...

AProVE
 Referenced in 144 articles
[sw07831]
 most powerful systems for automated termination proofs of term rewrite systems (TRSs ... completely flexible combination of different termination proof techniques. Due to this framework, AProVE...

VAMPIRE
 Referenced in 229 articles
[sw02918]
 theorem is proved, the system produces a verifiable proof, which validates both the clausification phase...

IMPS
 Referenced in 49 articles
[sw09143]
 IMPS: An interactive mathematical proof system. IMPS is an interactive mathematical proof system intended ... process and human comprehension of the resulting proofs. An initial theory library contained over...

ETPS
 Referenced in 152 articles
[sw06302]
 deductive information systems for these disciplines, expert systems which can reason, and certain aspects ... facilities for searching for expansion proofs, translating these into natural deduction proofs, constructing natural deduction ... facilities of TPS for constructing natural deduction proofs have been used under the name ETPS ... report ETPS: A System to Help Students Write Formal Proofs (postscript...

LCF
 Referenced in 157 articles
[sw08360]
 short history. The original LCF system was a proofchecking program developed at Stanford University ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed ... underlying it and the innovative polymorphic type system used both...

Proof General
 Referenced in 53 articles
[sw04901]
 currently used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others ... give a brief overview of what Proof General does and the philosophy behind it; technical...

HOL Light
 Referenced in 285 articles
[sw06580]
 overview. HOL Light is an interactive proof assistant for classical higherorder logic, intended ... version of Mike Gordon’s original HOL system. Theorem provers in this family ... this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...

OTTER
 Referenced in 310 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder logic ... strategies for directing and restricting searches for proofs. Otter can also be used ... calculator and has an embedded equational programming system. Otter is a fourthgeneration Argonne National...

ML
 Referenced in 502 articles
[sw01218]
 polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... ensures type safety – there is a formal proof that a welltyped ML program does...

SETHEO
 Referenced in 119 articles
[sw00707]
 systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure ... application of proof schemata are offered as options. The entire system is implemented...

LambdaClam
 Referenced in 24 articles
[sw19614]
 LambdaClam ( λclam, lclam) is a proof planning system that support proof planning over higherorder ... domains: System description: Proof planning in higherorder logic with λClam. This system description outlines ... λClam system for proof planning in higherorder logic. The usefulness and feasibility of applying ... higherorder proof planning to a number of types of problem is outlined, in particular...

KARO
 Referenced in 22 articles
[sw03116]
 also yielded a rather nonstandard proof system for the logic including socalled ... much more standard complete proof system (3) does not suffer from strange properties regarding sequentially...