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

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

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...

BliStr
 Referenced in 16 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 281 articles
[sw00060]
 ACL2 is both a programming language in which...

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

Isabelle
 Referenced in 639 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 51 articles
[sw00573]
 Many inequalities involving the functions ln, exp, sin...

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

PERL
 Referenced in 268 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 45 articles
[sw02589]
 MPTP 0.2: Design, implementation, and initial experiments. This...

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

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

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

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