Efficient formal verification of bounds of linear programs

DOI10.1007/978-3-642-22673-1_9zbMATH Open1335.68238OpenAlexW93453024MaRDI QIDQ5200112FDOQ5200112

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

Recommendations

• Theorem Proving in Higher Order Logics
• Formal Proofs for Nonlinear Optimization
• scientific article; zbMATH DE number 1614683
• A formal proof of the Kepler conjecture
• Flyspecking Flyspeck

Mathematics Subject Classification ID

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

Cites Work

• A proof of the Kepler conjecture
• Title not available (Why is that?)
• Title not available (Why is that?)
• Flyspeck II: The basic linear programs
• Linear Programs for the Kepler Conjecture

Cited In (8)

• Formal Proofs for Nonlinear Optimization
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• A new PCP outer verifier with applications to homogeneous linear equations and max-bisection
• On verified numerical computations in convex programming
• Title not available (Why is that?)
• Logic Based Program Synthesis and Transformation
• Affine Arithmetic and Applications to Real-Number Proving
• A FORMAL PROOF OF THE KEPLER CONJECTURE

Uses Software

• GLPK
• HOL Light
• Flyspeck
• kepler98

This page was built for publication: Efficient formal verification of bounds of linear programs

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