[[email protected]: [isabelle] MetiTarski theorem prover]
Piotr Rudnicki <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
----- Forwarded message from Lawrence Paulson <[email protected]> ----- From: Lawrence Paulson <[email protected]> To: [email protected], [email protected], [email protected] 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