
Nitpick
 Referenced in 61 articles
[sw00622]
 finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally...

CoCasl
 Referenced in 26 articles
[sw13076]
 systems in terms of inductive datatypes as well as of coinductive process types. Here...

Coq
 Referenced in 1784 articles
[sw00161]
 Coq is a formal proof management system. It...

ML
 Referenced in 514 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

PVS
 Referenced in 614 articles
[sw03484]
 PVS is a verification system: that is, a...

Haskell
 Referenced in 844 articles
[sw03521]
 Haskell is a standardized, generalpurpose purely functional...

SMTLIB
 Referenced in 182 articles
[sw04103]
 SMTLIB was created with the expectation that...

z3
 Referenced in 496 articles
[sw04887]
 Z3 is a highperformance theorem prover being...

HOL
 Referenced in 502 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

Sledgehammer
 Referenced in 119 articles
[sw07047]
 Sledgehammer is a tool that harnesses external first...

OEIS
 Referenced in 3387 articles
[sw07248]
 The OnLine Encyclopedia of Integer Sequence. The...

LCF
 Referenced in 157 articles
[sw08360]
 Edinburgh LCF. A mechanized logic of computation. From...

StarExec
 Referenced in 35 articles
[sw08839]
 StarExec: Starexec is a cross community logic solving...

CVC4
 Referenced in 104 articles
[sw09485]
 CVC4 is an efficient opensource automatic theorem...

Agda
 Referenced in 182 articles
[sw09689]
 Agda is a dependently typed functional programming language...

RADA
 Referenced in 4 articles
[sw20732]
 RADA: a tool for reasoning about algebraic data...

GitHub
 Referenced in 1503 articles
[sw23170]
 GitHub (originally known as Logical Awesome LLC)[3...