Flyspeck II: The basic linear programs

Steven Obua; Tobias Nipkow

doi:10.1007/s10472-009-9168-z

Flyspeck II: The basic linear programs

Steven Obua
, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Saarland University

Research output: Contribution to journal › Article › peer-review

9 Scopus citations

Abstract

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

Original language	English
Pages (from-to)	245-272
Number of pages	28
Journal	Annals of Mathematics and Artificial Intelligence
Volume	56
Issue number	3-4
DOIs	https://doi.org/10.1007/s10472-009-9168-z
State	Published - 2009

Keywords

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

Access to Document

10.1007/s10472-009-9168-z

Cite this

@article{a9fffdad83384759be9a8a354d0335b0,

title = "Flyspeck II: The basic linear programs",

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

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

author = "Steven Obua and Tobias Nipkow",

year = "2009",

doi = "10.1007/s10472-009-9168-z",

language = "English",

volume = "56",

pages = "245--272",

journal = "Annals of Mathematics and Artificial Intelligence",

issn = "1012-2443",

publisher = "Springer Netherlands",

number = "3-4",

}

TY - JOUR

T1 - Flyspeck II

T2 - The basic linear programs

AU - Obua, Steven

AU - Nipkow, Tobias

PY - 2009

Y1 - 2009

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

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

KW - Computational logic

KW - Finite matrices

KW - Flyspeck

KW - Higher-order logic

KW - Hypermaps

KW - Interactive theorem proving

KW - Isabelle

KW - Kepler conjecture

KW - Lattice-ordered rings

KW - Linear programming

KW - Planar graphs

UR - https://www.scopus.com/pages/publications/77949772715

U2 - 10.1007/s10472-009-9168-z

DO - 10.1007/s10472-009-9168-z

M3 - Article

AN - SCOPUS:77949772715

SN - 1012-2443

VL - 56

SP - 245

EP - 272

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

IS - 3-4

ER -

Flyspeck II: The basic linear programs

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this