Real algebraic strategies for MetiTarski proofs. (English) Zbl 1360.68764

Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo

Jeuring, Johan (ed.) et al., Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8–13, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31373-8/pbk). Lecture Notes in Computer Science 7362. Lecture Notes in Artificial Intelligence, 358-370 (2012).

Summary: MetiTarski [B. Akbarpour and L. C. Paulson, J. Autom. Reasoning 44, No. 3, 175–205 (2010; Zbl 1215.68206)] 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.
For the entire collection see [Zbl 1245.68013].

MSC:

68T15

Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 1215.68206

Software:

RealPaver; QEPCAD; MetiTarski