University of Cambridge > > Computer Laboratory Wednesday Seminars > MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions

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

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Mateja Jamnik.

Logical formulas 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. (This theory in particular includes the real numbers with addition, subtraction and multiplication.) Special functions are approximated by upper and lower bounds, which are typically ratios of polynomials. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts; the net effect is to split the problem into numerous cases, each covered by a different approximation, and to prove them individually. MetiTarski simplifies arithmetic expressions by conversion to a recursive representation, followed by flattening of nested quotients. It can solve many difficult problems found in mathematics reference works, and it can also solve problems that arise from hybrid and control systems.

This talk is part of the Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity