Email Gateway (Aug 19 2022 at 10:23): Email Gateway (Aug 19 2022 at 10:23):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.1 supports SMTLIB format for input files, as an alternative to the non-standard variant of TPTP that is normally used. Experimental code allowing Mathematica to reason directly about special functions has also been added. As always, thanks go to the development team, James Bridge in particular. Please see the release notes for details.
We continue to provide a binary distribution (64-bit Linux). And since QEPCAD is now optional, Windows users can finally build MetiTarski.
Please note that MetiTarski is experimental research software. Feedback is welcome!!
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC