Email Gateway (Aug 19 2022 at 11:17): Email Gateway (Aug 19 2022 at 11:17):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.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
Last updated: Nov 21 2024 at 12:39 UTC