[isabelle] MetiTarski 1.4 released!

pvs at csl.sri.com, isabelle-users at cl.cam.ac.uk, hol-info at lists.sourceforge.net, om-announce at openmath.org, theorem-provers at ai.mit.edu

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


This version includes support for problems involving existential quantifiers, the hyperbolic function tanh, etc.

Please note that MetiTarski is experimental research software and will require a certain amount of effort to build on your machine. Feedback would be welcome.

Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.