Automated Formal Proofs for Polynomial and Transcendental Problems

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

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.