[Om-announce] MetiTarski 2.1 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.1 supports SMTLIB format for input files, as an alternative to the non-standard variant of TPTP that is normally used. Experimental code allowing Mathematica to reason directly about special functions has also been added. As always, thanks go to the development team, James Bridge in particular. Please see the release notes for details.

We continue to 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