Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] MetiTarski 2.3 released!


view this post on Zulip Email Gateway (Aug 19 2022 at 13:58):

From: Lawrence Paulson <lp15@cam.ac.uk>
MetiTarski is an automatic theorem prover based on a combination of resolution and computer algebra technology. It is designed to prove theorems involving real-valued special functions such as ln, exp, sin, cos, arctan and sqrt. All variables are assumed to range over the real numbers.

MetiTarski can be downloaded from

http://www.cl.cam.ac.uk/~lp15/papers/Arith/download.html

You will be asked to leave your name and e-mail address so that we can have an idea how many users there are. You will not receive regular e-mails from us.

Version 2.3 supports user-defined functions (abbreviations introduced using axioms). Also, autoconf is now used to automatically configure builds on a variety of UNIX environments.

We continue to provide a binary distribution (64-bit Linux and OSX).

Please note that MetiTarski is experimental research software. Feedback is welcome!!

Larry Paulson


Last updated: Apr 23 2024 at 20:15 UTC