
Flyspeck
 Referenced in 124 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...

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

Tame Graphs
 Referenced in 16 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...

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

PRocH
 Referenced in 12 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...

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

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

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

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

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

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

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

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

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

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

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

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

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

SDPA
 Referenced in 187 articles
[sw03275]
 SDPA (SemiDefinite Programming Algorithm)” is one of the...