Flyspeck II: The basic linear programs

Steven Obua, Tobias Nipkow

Research output: Contribution to journalArticlepeer-review

8 Scopus citations

Abstract

We present another step, Flyspeck II, towards a complete, formal and mechanized proof of the Kepler Conjecture.

Original languageEnglish
Pages (from-to)245-272
Number of pages28
JournalAnnals of Mathematics and Artificial Intelligence
Volume56
Issue number3-4
DOIs
StatePublished - 2009

Keywords

  • Computational logic
  • Finite matrices
  • Flyspeck
  • Higher-order logic
  • Hypermaps
  • Interactive theorem proving
  • Isabelle
  • Kepler conjecture
  • Lattice-ordered rings
  • Linear programming
  • Planar graphs

Fingerprint

Dive into the research topics of 'Flyspeck II: The basic linear programs'. Together they form a unique fingerprint.

Cite this