• Coq

  • Referenced in 1748 articles [sw00161]
  • formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... semi-interactive development of machine-checked 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 ... semi-automated 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 proof-carrying-code 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 Martin-Lö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 proof-checking 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 higher-order 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 first-order 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 fourth-generation 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 well-typed 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...
  • Lambda-Clam

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

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