• HOL

  • Referenced in 583 articles [sw05492]
  • which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem...
  • HOL Light

  • Referenced in 307 articles [sw06580]
  • kernel. Despite this, it provides powerful proof tools and has been applied to some...
  • Isabelle/HOL

  • Referenced in 1018 articles [sw01569]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... formal language and provides tools for proving those formulas in a logical calculus. The main ... application is the formalization of mathematical proofs and in particular formal verification, which includes proving...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... formal language and provides tools for proving those formulas in a logical calculus. The main ... application is the formalization of mathematical proofs and in particular formal verification, which includes proving...
  • Proof General

  • Referenced in 53 articles [sw04901]
  • Proof General: A generic tool for proof development. This note describes Proof General, a tool...
  • ProofPower

  • Referenced in 57 articles [sw06339]
  • ProofPower is a specification and proof tool based on an implementation of Higher Order Logic ... proof in Z using a semantic embedding of Z into HOL. The DAZ tool supporting...
  • KRAKATOA

  • Referenced in 89 articles [sw03159]
  • three distinct components: the WHY tool, which computes proof obligations for a core imperative language ... conducting the development of proofs, and finally the KRAKATOA tool, a translator...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack ... LEGO is a powerful tool for interactive proof development in the natural deduction style...
  • Hets

  • Referenced in 61 articles [sw07017]
  • parsing, static analysis and proof management tool incorporating various provers and different specification languages, thus...
  • AProVE

  • Referenced in 160 articles [sw07831]
  • automated termination proofs of term rewrite systems (TRSs). It is the first tool which automates ... completely flexible combination of different termination proof techniques. Due to this framework, AProVE...
  • DRAT-trim

  • Referenced in 36 articles [sw13313]
  • trimming using expressive clausal proofs. The DRAT-trim tool is a satisfiability proof checker based ... hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized ... proofs, and new TraceCheck$^{ + }$ dependency graphs. We describe the output that is produced, what optimizations ... clauses, and potential applications of the tool...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics. The Emacs ... MizarMode and focuses on the proof assistance functions and tools available ... learning tools like the Mizar Proof Advisor, deductive tools like MoMM ... give an overview of these proof-assistance tools and their integration in the MizarMode...
  • CARIBOO

  • Referenced in 14 articles [sw10064]
  • CARIBOO: a multi-strategy termination proof tool based on induction. A termination proof tool ... based programs CARIBOO is a termination proof tool for rule-based programming languages, where ... contrast with most of the existing tools, which prove in general termination of standard rewriting ... free term algebra, our proof tool, named CARIBOO (for Computing AbstRaction for Induction Based termination...
  • Timbuk

  • Referenced in 47 articles [sw06351]
  • Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems ... Older Timbuk distributions (2.2) provide three standalone tools and a bunch of Objective Caml functions...
  • EasyCrypt

  • Referenced in 32 articles [sw09738]
  • present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches ... then compiled into verifiable proofs in the CertiCrypt framework. The tool supports most common reasoning ... cryptographers and illustrate its application to security proofs of the Cramer-Shoup and Hashed ElGamal...
  • Matita

  • Referenced in 71 articles [sw06140]
  • prover is a software tool aiding the development of formal proofs by man-machine collaboration...
  • SymbolicData

  • Referenced in 28 articles [sw04621]
  • common data base of proof schemes, and to develop tools to extract examples, prepare them ... collection with more than 500 examples of proof schemes, was their restricted availability and interoperability ... publicly available repository, and tools to prepare these generic proof schemes for input to different...
  • Sledgehammer

  • Referenced in 137 articles [sw07047]
  • tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations...
  • CalcCheck

  • Referenced in 40 articles [sw09760]
  • teaching tool CalcCheck: a proof-checker for Gries and Schneider’s “logical approach to discrete...
  • CeTA

  • Referenced in 47 articles [sw06584]
  • Certification of termination proofs using CeTA. There are many automatic tools to prove termination ... these tools use a combination of many complex termination criteria. Hence generated proofs...