Sciweavers

Share
AISC
2008
Springer

MetiTarski: An Automatic Prover for the Elementary Functions

9 years 5 months ago
MetiTarski: An Automatic Prover for the Elementary Functions
Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure (QEPCAD) for the theory of real closed fields. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts, while deleting as redundant clauses that follow algebraically from other clauses. MetiTarski includes special code to simplify arithmetic expressions.
Behzad Akbarpour, Lawrence C. Paulson
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AISC
Authors Behzad Akbarpour, Lawrence C. Paulson
Comments (0)
books