Flyspeck II: The basic linear programs

DOI10.1007/S10472-009-9168-ZMaRDI QIDQ2379683zbMATH OpenOpenAlexFDO

Authors Steven Obua, Tobias Nipkow

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Linear programming (90C05)

Recommendations

• Linear Programming
• scientific article; zbMATH DE number 4020840
• scientific article; zbMATH DE number 1163804
• scientific article; zbMATH DE number 1421685
• scientific article; zbMATH DE number 2166871
• scientific article; zbMATH DE number 3934758
• Solving linear programs with finite precision. II: Algorithms
• Linear Programming from Fibonacci to Farkas

Cites work

• A Compiled Implementation of Normalization by Evaluation
• A formulation of the Kepler conjecture
• A proof of the Kepler conjecture
• A revision of the proof of the Kepler conjecture
• Flyspeck I: Tame Graphs
• Flyspeck II: The basic linear programs
• Formal proof - the four color theorem
• scientific article; zbMATH DE number 1670733 (Why is no real title available?)
• scientific article; zbMATH DE number 5614797 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 2003148 (Why is no real title available?)
• scientific article; zbMATH DE number 3245483 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Partial Recursive Functions in Higher-Order Logic
• Proof Pearl: Looping Around the Orbit
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
• Two Fast Algorithms for Sparse Matrices: Multiplication and Permuted Transposition
• Types for Proofs and Programs

Cited in

(13)

• Formalization of function matrix theory in HOL
• 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
• Verified efficient enumeration of plane graphs modulo isomorphism
• The Isabelle Framework
• The dodecahedral conjecture
• Efficient formal verification of bounds of linear programs
• A formal proof of the Kepler conjecture
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting
• Effective homology of bicomplexes, formalized in Coq
• Linear Programming
• Generating certified code from formal proofs: a case study in homological algebra
• A revision of the proof of the Kepler conjecture

Describes a project that uses

Uses Software

• Tame Graphs
• kepler98
• LCF
• Flyspeck
• Coq
• Isar

This page was built for publication: Flyspeck II: The basic linear programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2379683)