[mizar] [lp15@cam.ac.uk: [isabelle] MetiTarski theorem prover]

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

----- Forwarded message from Lawrence Paulson <lp15@cam.ac.uk> -----

From: Lawrence Paulson <lp15@cam.ac.uk>
To: pvs@csl.sri.com, isabelle-users@cl.cam.ac.uk,
	hol-info@lists.sourceforge.net
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.tgz
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html

Please 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