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.

• Type: Conference
• Year: 2008
• Where: AISC
• Authors: Behzad Akbarpour, Lawrence C. Paulson
• Keywords: AISC 2008, Artificial Intelligence, Decision Procedure, Procedure Simplifies Clauses, Resolution Theorem Prover