Email Gateway (Aug 18 2022 at 13:55): Email Gateway (Aug 18 2022 at 13:55):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: May 03 2024 at 08:18 UTC