MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions |
| |
Authors: | Behzad Akbarpour Lawrence Charles Paulson |
| |
Affiliation: | 1.Computer Laboratory,University of Cambridge,Cambridge,UK |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|