
Flyspeck
 Referenced in 98 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 14 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 18 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 13 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 256 articles
[sw00060]
 ACL2 is both a programming language in which...

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

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

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

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

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

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

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

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

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

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

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

SPASS
 Referenced in 154 articles
[sw04108]
 SPASS is an automated theorem prover for first...