Ceci est une ancienne révision du document !


Automatic theorem provers

MetiTarski

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 real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. This problem is undecidable, so MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful.

 
automatic_theorem_provers.1383563457.txt.gz · Dernière modification: Le 04/11/2013 à 12:10 par david_mentre     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó