• Coq

  • Referenced in 1818 articles [sw00161]
  • formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... environment for semi-interactive development of machine-checked 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 ... semi-automated 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 proof-checking program developed at Stanford University ... proof assistant for higher order logic originally developed for reasoning about hardware.2 The multi-faceted ... 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]
  • cross-linking 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 fourth-generation 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 Hoare-style 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...
  • Leo-III

  • Referenced in 14 articles [sw18516]
  • developed. Leo-III combines its predecessor’s concept of cooperating external specialist systems with ... novel agent-based 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 proof-by-pointing, 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, rule-based 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...