[Om-announce] MetiTarski 2.3 released!

Lawrence Paulson lp15 at cam.ac.uk
Tue Mar 4 17:09:28 CET 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.3 supports user-defined functions (abbreviations introduced using axioms). Also, autoconf is now used to automatically configure builds on a variety of UNIX environments.

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