
HOL
 Referenced in 583 articles
[sw05492]
 which theorems can be proved and proof tools implemented. Builtin 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...

DRATtrim
 Referenced in 36 articles
[sw13313]
 trimming using expressive clausal proofs. The DRATtrim tool is a satisfiability proof checker based ... hurdle of resolutionbased proof checkers. The DRATtrim 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 proofassistance tools and their integration in the MizarMode...

CARIBOO
 Referenced in 14 articles
[sw10064]
 CARIBOO: a multistrategy termination proof tool based on induction. A termination proof tool ... based programs CARIBOO is a termination proof tool for rulebased 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 CramerShoup and Hashed ElGamal...

Matita
 Referenced in 71 articles
[sw06140]
 prover is a software tool aiding the development of formal proofs by manmachine 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 firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations...

CalcCheck
 Referenced in 40 articles
[sw09760]
 teaching tool CalcCheck: a proofchecker 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...