Sciweavers

Share
JAR
2010

MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions

9 years 21 days ago
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions
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.
Behzad Akbarpour, Lawrence C. Paulson
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JAR
Authors Behzad Akbarpour, Lawrence C. Paulson
Comments (0)
books