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

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