MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions
复制标题
DOI：
10.1007/s10817-009-9149-2
复制
发表时间：
2010-03-01
期刊：
影响因子：
--
通讯作者：
Paulson, Lawrence Charles
中科院分区：
文献类型：
--
作者：
Akbarpour, Behzad;Paulson, Lawrence Charles
许多涉及特殊函数如ln、exp和sin的定理可以由MetiTarski自动证明：一个修改为调用真实的闭域理论的判定过程的分解定理证明器。特殊函数由上界和下界近似，通常是从泰勒或连分式展开导出的有理函数。判定过程通过删除与其他代数事实不一致的文字来简化子句。MetiTarski通过将算术表达式转换为递归表示来简化算术表达式，然后对嵌套的递归项进行扁平化。应用包括验证混合动力和控制系统。
Many theorems involving special functions such as ln, exp and sin can be proved automatically by MetiTarski: a resolution theorem prover modified to call a decision procedure for the theory of real closed fields. Special functions are approximated by upper and lower bounds, which are typically rational functions derived from Taylor or continued fraction expansions. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts. MetiTarski simplifies arithmetic expressions by conversion to a recursive representation, followed by flattening of nested quotients. Applications include verifying hybrid and control systems.