• 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 non-trivial 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...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based 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 general-purpose 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...