Automated Formal Proofs for Polynomial and Transcendental Problems

多项式和超越问题的自动形式证明

• 批准号: EP/G002290/1
• 负责人: Lawrence Paulson
• 金额: $ 11.01万
• 依托单位: University of Cambridge
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2008
• 资助国家: 英国
• 起止时间: 2008 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FG002290%2F1
• 关键词: Automated; Formal; Proofs; Polynomial; Transcendental

Many applications in science and engineering involve mathematical formulas. Such formulas may involve polynomials, logarithms, exponentials and related functions, perhaps combined using logical symbols to express conditional statements. No automatic procedure exists for solving such problems in the general case. Where automatic procedures do exist, they are often far too expensive (in terms of computer time and memory requirements) to use in practice. However, a judicious selection of specialised procedures can yield efficient solutions for many problems that arise in practice. The proposal is to identify and implement variety of such procedures.This work will be undertaken in the context of software tools known as interactive theorem provers. These tools perform logical deductions to be very high degree of reliability; they are increasingly being utilised to help assure correctness for safety critical applications. A primary challenge of this project is to reconcile the detailed low-level checking used in interactive theorem provers with the high-level reasoning typical of most approaches to solving mathematical formulas. One fruitful technique is to deliver evidence from the mathematical solver to the interactive theorem prover: for some types of problems, finding the solution is difficult, but verifying a claimed solution is easy.

科学和工程中的许多应用都涉及数学公式。这样的公式可能涉及多项式、对数、指数和相关函数，可能使用逻辑符号组合起来表示条件语句。在一般情况下，不存在解决此类问题的自动程序。在确实存在自动程序的地方，它们往往过于昂贵(就计算机时间和内存要求而言)，无法在实践中使用。然而，明智地选择专门的程序可以为实践中出现的许多问题提供有效的解决方案。这项工作将在被称为交互式定理证明器的软件工具的背景下进行。这些工具执行非常高的可靠性的逻辑推理；它们越来越多地被用来帮助确保安全关键应用的正确性。这个项目的一个主要挑战是协调交互式定理证明器中使用的详细的低级检查与大多数求解数学公式的方法中典型的高级推理。一种卓有成效的技术是将证据从数学求解器传递给交互定理证明者：对于某些类型的问题，找到解决方案很困难，但验证声称的解决方案很容易。