Email Gateway (Aug 18 2022 at 15:21): Email Gateway (Aug 18 2022 at 15:21):From: Lawrence Paulson <lp15@cam.ac.uk>
pvs@csl.sri.com, isabelle-users@cl.cam.ac.uk, hol-info@lists.sourceforge.net, om-announce@openmath.org, theorem-provers@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
http://www.cl.cam.ac.uk/~lp15/papers/Arith/metit-1.4.tgz
http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html
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
Last updated: Apr 23 2024 at 16:19 UTC