• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Intelligent computer mathematics >Certification of Bounds of Non-linear Functions: The Templates Method
【24h】

Certification of Bounds of Non-linear Functions: The Templates Method

机译：非线性函数边界的证明：模板方法

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually, formally provable in a proof system such as Coq. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of inequalities. We introduce an approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis). This algorithm consists in bounding some of the constituents of the function by suprema of quadratic forms with a well chosen curvature. This leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Templates limit the blow up of these relaxations at the price of coarsening the approximation. We illustrate the efficiency of our framework with various examples from the literature and discuss the interfacing with Coq.
机译：这项工作的目的是证明由半代数或超越表达式定义的实值多元函数的下界。最终，该证书必须在证明系统（例如Coq）中得到正式证明。这种工具的应用范围广泛。例如，海尔斯（Hales）对开普勒猜想的证明产生了数千个不平等。我们介绍一种近似算法，该算法结合了最大加基法（在最佳控制中）和Manna等人开发的线性模板法的思想。 （在静态分析中）。该算法包括通过选择具有良好曲率的二次形式的极值来界定函数的某些组成部分。这将导致半代数优化问题，并通过平方和松弛来解决。模板以粗化近似值为代价来限制这些松弛的爆发。我们使用文献中的各种示例来说明我们框架的效率，并讨论与Coq的接口。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号