Efficient formal verification of bounds of linear programs

DOI10.1007/978-3-642-22673-1_9MaRDI QIDQ5200112zbMATH OpenOpenAlexFDO

Authors Alexey Solovyev, Thomas C. Hales

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)

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

Cites work

• scientific article; zbMATH DE number 1042857 (Why is no real title available?)
• A proof of the Kepler conjecture
• Flyspeck II: The basic linear programs
• Formal proof - the four color theorem
• Linear Programs for the Kepler Conjecture

Cited in

(9)

• 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
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 1614683 (Why is no real title available?)
• A new PCP outer verifier with applications to homogeneous linear equations and max-bisection
• Logic Based Program Synthesis and Transformation
• On verified numerical computations in convex programming
• Affine arithmetic and applications to real-number proving
• Formal Proofs for Nonlinear Optimization

Describes a project that uses

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)