[isabelle] MetiTarski 2.4 released!

MetiTarski is an automatic theorem prover based on a combination of resolution and computer algebra technology. It is designed to prove theorems involving real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All variables are assumed to range over the real numbers.

MetiTarski can be downloaded from 


You will be asked to leave your name and e-mail address so that we can have an idea how many users there are. You will not receive regular e-mails from us.

Version 2.4 includes improved documentation, the nth-root function and experimental support for Bessel functions of the first kind. We have added over 30,000 problems arising from William Denman's Ph.D. research.

We continue to provide a binary distribution (64-bit Linux and OSX).

Please note that MetiTarski is experimental research software. Feedback is welcome!!

Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.