Efficient Formal Verification of Bounds of Linear Programs

DOI10.1007/978-3-642-22673-1_9zbMath1335.68238OpenAlexW93453024MaRDI QIDQ5200112

Thomas C. Hales, Alexey Solovyev

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_9

Mathematics Subject Classification ID

Numerical mathematical programming methods (65K05) Linear programming (90C05)

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, Affine Arithmetic and Applications to Real-Number Proving

Uses Software

• GLPK
• HOL Light
• Flyspeck
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Flyspeck II: The basic linear programs
• A proof of the Kepler conjecture
• Linear Programs for the Kepler Conjecture