[Om-announce] MetiTarski 2.4 released!

Lawrence Paulson lp15 at cam.ac.uk
Wed Oct 22 13:33:56 CEST 2014

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

More information about the Om-announce mailing list