[Om-announce] MetiTarski 2.0 released!

[Lawrence Paulson]

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 

	http://www.cl.cam.ac.uk/~lp15/papers/Arith/download.html

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.0 includes numerous improvements over the previous version. In particular, we now allow Z3 and Mathematica as decision procedures, as alternatives to QEPCAD. These allow much more difficult problems to be solved than hitherto. This is the result of hard work by the development team, in particular, James Bridge and Grant Passmore. Please see the release notes for details.

For the first time, we provide a binary distribution (64-bit Linux). And since QEPCAD is now optional, Windows users can finally build MetiTarski.

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

Larry Paulson