[Om-announce] MetiTarski theorem prover (Version 1.2)

Lawrence Paulson lp15 at cam.ac.uk
Tue Aug 11 16:25:35 CEST 2009


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.2.tgz
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html

This version includes support for the TPTP "include" directive and  
many new problems on analogue circuit verification, etc., from  
Concordia University.

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




More information about the Om-announce mailing list