Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] MetiTarski 1.5 released!

view this post on Zulip Email Gateway (Aug 18 2022 at 15:44):

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

This version includes improved heuristics and data structures, giving somewhat better performance, and includes some new and corrected problems.

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 19 2024 at 16:20 UTC