
Flyspeck
 Referenced in 107 articles
[sw10277]
 Communicating formal proofs: the case of flyspeck. We introduce a platform for presenting and cross ... developments. As an example, we show the Flyspeck formal development (in HOL Light ... Flyspeck informal mathematical text as a narrative linked to the formal development. To make this...

Tame Graphs
 Referenced in 15 articles
[sw28578]
 Flyspeck I: Tame Graphs. These theories present the verified enumeration of tame plane graphs ... tameness are identical to those in the Flyspeck project. The IJCAR 2006 paper by Nipkow...

HOLyHammer
 Referenced in 20 articles
[sw11553]
 answering include the recent versions of the Flyspeck, Multivariate Analysis and Complex Analysis libraries...

PRocH
 Referenced in 11 articles
[sw10191]
 recently developed translation of HOL Light and Flyspeck problems to ATP formats. PRocH combines several ... evaluated here on a large set of Flyspeck problems...

BliStr
 Referenced in 15 articles
[sw16818]
 obtained on the problems created from the Flyspeck corpus...

NLCertify
 Referenced in 4 articles
[sw08786]
 solves successfully nontrivial inequalities from the Flyspeck project (essentially tight inequalities, involving both semialgebraic...

ACL2
 Referenced in 273 articles
[sw00060]
 ACL2 is both a programming language in which...

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

Isabelle
 Referenced in 591 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEOII
 Referenced in 49 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

MetiTarski
 Referenced in 49 articles
[sw00573]
 Many inequalities involving the functions ln, exp, sin...

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

PERL
 Referenced in 254 articles
[sw01225]
 Programming Perl. Perl is a language for easily...

MPTP
 Referenced in 22 articles
[sw02489]
 We describe a number of new possibilities for...

MPTP 0.2
 Referenced in 43 articles
[sw02589]
 MPTP 0.2: Design, implementation, and initial experiments. This...

OTTER
 Referenced in 310 articles
[sw02904]
 Our current automated deduction system Otter is designed...

VAMPIRE
 Referenced in 227 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

KRAKATOA
 Referenced in 85 articles
[sw03159]
 The KRAKATOA tool for certification of JAVA/JAVACARD programs...

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