基于泰勒区间逼近的非线性不等式形式化验证
计算机科学中的逻辑
2013-05-22 v1 逻辑
摘要
我们提出了一种用于验证多元非线性不等式的形式化工具。我们的验证方法基于带有泰勒逼近的区间算术。该工具在 HOL Light 证明助手中实现，能够验证矩形域上的多元非线性多项式及非多项式不等式。我们工作的主要特点之一是验证过程的高效实现，能够在数秒内证明非平凡的高维不等式。我们开发此验证工具作为 Flyspeck 项目（开普勒猜想的形式化证明）的一部分。Flyspeck 项目包含约 1000 个非线性不等式。我们成功地在 100 多个 Flyspeck 不等式上测试了该方法，并估计形式化验证过程比用 C++ 实现的非形式化验证方法慢约 3000 倍。我们还描述了该方法的未来工作和潜在的优化方向。
引用
@article{arxiv.1301.1702,
title = {Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations},
author = {Alexey Solovyev and Thomas C. Hales},
journal= {arXiv preprint arXiv:1301.1702},
year = {2013}
}
备注
15 pages