Proving Bounds for Real Linear Programs in Isabelle/HOL
Proving Bounds for Real Linear Programs in Isabelle/HOL
复制标题
DOI：
10.1007/11541868_15
复制
发表时间：
2005-08
期刊：
影响因子：
--
通讯作者：
Steven Obua
中科院分区：
文献类型：
--
作者：
Steven Obua
线性规划是一种基本的数学技术，用于在线性不等式约束的域上优化线性函数。我们将自己限制为只涉及实变量的有界域上的线性规划。在定理证明的上下文中，这个限制使得任何给定的线性规划都有可能从外部线性规划工具获得证书，这些证书有助于证明给定线性规划的任意精确边界。为此，提出了矩阵在Isabelle/HOL中的显式形式化，以及格序环的概念如何允许矩阵与Isabelle的公理类型类的平滑积分。由于我们的工作是对Flyspeck项目的贡献，我们认为，利用上述技术，现在可以足够快地证明开普勒猜想证明中出现的线性程序的边界。
Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve only real variables. In the context of theorem proving, this restriction makes it possible for any given linear program to obtain certificates from external linear programming tools that help to prove arbitrarily precise bounds for the given linear program. To this end, an explicit formalization of matrices in Isabelle/HOL is presented, and how the concept of lattice-ordered rings allows for a smooth integration of matrices with the axiomatic type classes of Isabelle.As our work is a contribution to the Flyspeck project, we argue that with the above techniques it is now possible to prove bounds for the linear programs arising in the proof of the Kepler conjecture sufficiently fast.