Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] MetiTarski theorem prover


view this post on Zulip Email Gateway (Aug 18 2022 at 12:42):

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

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: Nov 21 2024 at 12:39 UTC