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 ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
