
Isabelle/HOL
 Referenced in 945 articles
[sw01569]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

Isabelle
 Referenced in 606 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

Automath
 Referenced in 403 articles
[sw07127]
 type theoretical” line of proof assistants from which the better known current ones are Nuprl...

HOL Light
 Referenced in 288 articles
[sw06580]
 overview. HOL Light is an interactive proof assistant for classical higherorder logic, intended ... logical kernel. Despite this, it provides powerful proof tools and has been applied to some...

Agda
 Referenced in 182 articles
[sw09689]
 your code). Agda is also a proof assistant: It is an interactive system for writing ... many similarities with other proof assistants based on dependent types, such as Coq, Epigram...

LCF
 Referenced in 157 articles
[sw08360]
 history. The original LCF system was a proofchecking program developed at Stanford University ... form a thriving paradigm in computer assisted reasoning. Many of the developments of the last ... descendents of LCF is HOL, a proof assistant for higher order logic originally developed...

Archive Formal Proofs
 Referenced in 152 articles
[sw28613]
 computerchecked proofs developed using the proof assistant Isabelle. We perform an indepth analysis ... archive, looking at various properties of the proof developments, including size, dependencies, and proof style...

Isar
 Referenced in 140 articles
[sw04599]
 generic (X)Emacs interface for interactive proof assistants, we arrive at a reasonable environment...

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

KRAKATOA
 Referenced in 86 articles
[sw03159]
 postconditions, the CQQ proof assistant for modeling the program semantics and conducting the development...

Proof General
 Referenced in 53 articles
[sw04901]
 developing machine proofs with an interactive proof assistant. Interaction is based around a proof script ... effort, alleviating the need for a proof assistant to provide its own GUI, and providing ... uniform appearance for diverse proof assistants. par Proof General has a growing user base...

ALF
 Referenced in 67 articles
[sw08603]
 substitutions. ALF is a general purpose proof assistant, in which different logics can be represented...

Coq/SSReflect
 Referenced in 63 articles
[sw09360]
 Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale...

Isabelle/ZF
 Referenced in 62 articles
[sw04973]
 Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed ... main application is the formalization of mathematical proofs and in particular formal verification, which includes...

CoLoR
 Referenced in 38 articles
[sw09806]
 notably required for programs formulated in proof assistants. It is a very active subject ... wellfounded (rewrite) relations in the proof assistant Coq. We also present its application...

Ott
 Referenced in 30 articles
[sw00663]
 formal mathematics of a proof assistant  make it much harder than necessary to work with ... such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together ... binding structures; and (3) compilation to proof assistant code. This has been tested in substantial ... large fragment of OCaml, with mechanised proofs of various soundness results. Our aim with this...

Ynot
 Referenced in 35 articles
[sw12334]
 axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher...

MizarMode
 Referenced in 17 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 ... methods employed in tactical and programmable proof assistants, it makes the “proof code ... give an overview of these proofassistance tools and their integration in the MizarMode...

Jakarta
 Referenced in 18 articles
[sw01269]
 compiler that translates JSL specifications into proof assistants; the JaKarTa Automation Kit (JAK), a toolset ... support reasoning about executable specifications within proof assistants. Goal of the work is to derive...

MaSh
 Referenced in 21 articles
[sw08206]
 integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance ﬁlter ... MaSh, an alternative that learns from successful proofs. New challenges arose from our “zeroclick...