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

Add 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 Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.