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)
- Cambridge talks
- 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 talksSciScreen: Finding Dory Plants of the Richtersveld THE MATHEMATICAL MAGIC OF MIXED REALITY Polish Britain: Multilingualism and Diaspora Community Microtubule Modulation of Myocyte Mechanics An approach to the four colour theorem via Donaldson- Floer theory Computing knot Floer homology Changing understandings of the human fetus over five decades of legal abortion |