[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] MetiTarski theorem prover (Version 1.1)



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.1.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