Automatic Proof Procedures for Polynomials and Special Functions

多项式和特殊函数的自动证明程序

• 批准号: EP/I011005/1
• 负责人: Lawrence Paulson
• 金额: $ 67.94万
• 依托单位: University of Cambridge
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FI011005%2F1
• 关键词: Automatic; Proof; Procedures; Polynomials; Special

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.

工程设计应满足安全约束，其中许多约束可以用数学和逻辑公式来表示。现有的计算机软件可以自动检查一些这样的公式，但尽管它们可以具有庞大而复杂的逻辑结构，但数学部分目前必须是线性的：换句话说，除了加法之外，不涉及任何更复杂的内容。现实世界的工程问题涉及复杂的数学概念，如多项式和超越函数。研究人员开发了在许多情况下可以解决此类问题的软件(称为MetiTarski和RAHD)。目前的项目将扩大该软件的范围，增加其功能，并针对特定的现实世界应用领域。其中一个这样的应用是模拟电路，它在消费电子产品中很普遍。该项目将调查工程和数学科学中的许多其他潜在应用。

项目成果

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

• DOI: 10.1016/j.cl.2015.11.003
• 发表时间: 2017
• 期刊: Comput. Lang. Syst. Struct.
• 作者: Khalil Ghorbal;A. Sogokon;André Platzer

Static Analysis

静态分析

• DOI: 10.1007/978-3-642-38856-9_22
• 发表时间: 2013
• 作者: Brain M

Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions

实值特殊函数自动定理证明器中的案例分割

• DOI: 10.1007/s10817-012-9245-6
• 发表时间: 2012
• 期刊: Journal of Automated Reasoning
• 作者: Bridge J

Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

使用自动定理证明器对超越定点和浮点算法进行形式验证

• DOI: 10.1145/3543670
• 发表时间: 2022
• 期刊: Formal Aspects of Computing
• 影响因子: 1
• 作者: Coward S

Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings

自动演绎 - CADE-24 - 第 24 届国际自动演绎会议，美国纽约州普莱西德湖，2013 年 6 月 9 日至 14 日。会议记录

• DOI: 10.1007/978-3-642-38574-2_12
• 发表时间: 2013
• 作者: De Moura L