Automatic Proof Procedures for Polynomials and Special Functions

工程设计应满足安全约束，其中许多约束可以用数学和逻辑公式表示。现有的计算机软件可以自动检查一些这样的公式，但是，尽管它们可以有一个庞大而复杂的逻辑结构，但目前的数学成分必须是线性的：换句话说，不涉及比加法更复杂的东西。现实世界的工程问题涉及复杂的数学概念，如多项式和超越函数。研究人员已经开发了软件（名为MetiTarski和RAHD），可以在许多情况下解决这类问题。当前的项目将扩展该软件的范围，增加其功能并将其定位于特定的实际应用领域。其中一个应用是模拟电路，它在消费电子产品中广泛应用。该项目将研究在工程和数学科学中的许多其他潜在应用。

An engineering design is expected to satisfy safety constraints, many of which can be expressed as mathematical and logical formulas. Computer software exists that can check some such formulas automatically, but although they can have a large and complicated logical structure, the mathematical component currently has to be linear: in other words, involving nothing more complicated than addition. Real-world engineering problems involve sophisticated mathematical concepts, such as polynomials and transcendental functions.The investigators have developed software (called MetiTarski and RAHD) that can solve such problems in many cases. The current project will extend the scope of this software, increasing its power and targeting it at specific real-world application areas. One such application is analogue circuitry, which is widespread in consumer electronics. The project will investigate many other potential applications In engineering and the mathematical sciences.