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.2 is designed to work with the latest version of Z3. It includes a
number of modest changes compared with the previous version.
We are grateful to NASA's César Muñoz for building the ready to run binaries
(both for Linux and OS X). He comments,
> It includes a shell script "metit" that sets all the environment variables
> needed to execute the binaries metit and z3 in the directory bin. Please
> notice that you have to execute the shell script "metit" rather than the
> binary metit. You can add the distribution directory to your PATH, but it is
> not required.
Please note that MetiTarski is experimental research software. Feedback is
welcome!!
Larry Paulson
_______________________________________________
Om-announce mailing list
[email protected]
http://openmath.org/mailman/listinfo/om-announce
