Published in

Springer Verlag, Lecture Notes in Computer Science, p. 358-370

DOI: 10.1007/978-3-642-31374-5_24

Links

Tools

Export citation

Search in Google Scholar

Real Algebraic Strategies for MetiTarski Proofs

Proceedings article published in 2012 by Grant Olney Passmore, Lawrence C. Paulson, Leonardo de Moura, Leonardo Mendonça Moura
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Green circle
Postprint: archiving allowed
Upload
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

Abstract

MetiTarski [1] is an automatic theorem prover that can prove inequalities involving sin, cos, exp, ln, 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.