Real Algebraic Strategies for MetiTarski Proofs

摘要

MetiTarski [1] is an automatic theorem prover that can prove inequalities involving sin, cos, exp, In, etc. During its proof search, it generates a series of subproblems in nonlinear polynomial real arithmetic which are reduced to true or false using a decision procedure for the theory of real closed fields (RCF). These calls are often a bottleneck: RCF is fundamentally infeasible. However, by studying these subproblems, we can design specialised variants of RCF decision procedures that run faster and improve MetiTarski's performance.