From: Lawrence Paulson <lp15@cam.ac.uk>
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.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
Last updated: Nov 21 2024 at 12:39 UTC