----- Forwarded message from Lawrence Paulson <
lp15@...> -----
From: Lawrence Paulson <
lp15@...>
To:
pvs@...,
isabelle-users@...,
hol-info@...
Date: Tue, 2 Dec 2008 17:16:25 +0000
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.0.tgzhttp://www.cl.cam.ac.uk/~lp15/papers/Arith/index.htmlPlease note that it is experimental research software and will require
a certain amount of effort to build on your machine. Feedback would be
welcome.
Larry Paulson
----- End forwarded message -----
--
Piotr Rudnicki
http://web.cs.ualberta.ca/~piotr
