COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## MetiTarski: An Automatic Theorem Prover for Real-Valued Special FunctionsAdd to your list(s) Download to your calendar using vCal - Larry Paulson - Univ. of Cambridge Computer Laboratory
- Wednesday 26 November 2008, 14:15-15:15
- Lecture Theatre 1, Computer Laboratory.
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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Chris Davis' list
- Computer Laboratory Wednesday Seminars
- Computer Laboratory talks
- Graduate-Seminars
- Guy Emerson's list
- Interested Talks
- Lecture Theatre 1, Computer Laboratory
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- computer science
- se393's list
Note that ex-directory lists are not shown. |
## Other listsTagliaferri Lecture Cambridge University Library lunchtime talks Rethinking Life## Other talksPolish Britain: Multilingualism and Diaspora Community THE MATHEMATICAL MAGIC OF MIXED REALITY Plants of the Richtersveld SciScreen: Finding Dory Large scale vortices and zonal flows in spherical rotating convection Changing understandings of the human fetus over five decades of legal abortion |