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/. 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 1.9 represents over 6 months of development over the previous version, incorporating code by James Bridge and Grant Passmore, along with new problems supplied by William Denman. Please see the release notes for details.
Remark about CASC: The version run in the competition was 1.8. We did not push to release this version in time for CASC because most of our work would have been irrelevant. None of the problems used in the competition Involve real-valued special functions.
MetiTarski is experimental research software and may require a certain amount of effort to build on your machine.
technowlogies 