[Om-announce] MetiTarski 1.7 released!

Lawrence Paulson lp15 at cam.ac.uk
Mon Nov 1 13:13:59 CET 2010


MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving functions such as log, exp, sin, cos and sqrt. MetiTarski is available to download; see

http://www.cl.cam.ac.uk/~lp15/papers/Arith/metit-1.7.tgz
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html

This version introduces support for cube roots, with many new problems, as well as important bug fixes.

Please note that MetiTarski is experimental research software and will require a certain amount of effort to build on your machine. Feedback is welcome!!

Larry Paulson





More information about the Om-announce mailing list