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.