Flyspeck II: The basic linear programs
From MaRDI portal
Publication:2379683
DOI10.1007/s10472-009-9168-zzbMath1184.68465OpenAlexW2093262333MaRDI QIDQ2379683
Publication date: 19 March 2010
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: http://mediatum.ub.tum.de/doc/645669/document.pdf
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Flyspeck II: The basic linear programs ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Effective homology of bicomplexes, formalized in Coq ⋮ The Isabelle Framework ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ The dodecahedral conjecture ⋮ A revision of the proof of the Kepler conjecture ⋮ Efficient Formal Verification of Bounds of Linear Programs ⋮ Formalization of function matrix theory in HOL ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A formulation of the Kepler conjecture
- A revision of the proof of the Kepler conjecture
- Isabelle/HOL. A proof assistant for higher-order logic
- Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
- Flyspeck II: The basic linear programs
- A proof of the Kepler conjecture
- Proof Pearl: Looping Around the Orbit
- A Compiled Implementation of Normalization by Evaluation
- Flyspeck I: Tame Graphs
- Partial Recursive Functions in Higher-Order Logic
- Two Fast Algorithms for Sparse Matrices: Multiplication and Permuted Transposition
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
