MetiTarski: An automatic theorem prover for real-valued special functions. (English) Zbl 1215.68206

Akbarpour, Behzad; Paulson, Lawrence Charles

J. Autom. Reasoning 44, No. 3, 175-205 (2010).

Summary: Many theorems involving special functions such as ln, exp and sin can be proved automatically by MetiTarski: a resolution theorem prover modified to call a decision procedure for the theory of real closed fields. Special functions are approximated by upper and lower bounds, which are typically rational functions derived from Taylor or continued fraction expansions. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts. MetiTarski simplifies arithmetic expressions by conversion to a recursive representation, followed by flattening of nested quotients. Applications include verifying hybrid and control systems.

MSC:

68T15

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

Keywords:

resolution theorem prover

Software:

OTTER; HySAT; MetiTarski; QEPCAD; RSOLVER; HSolver; SPASS+T; Analytica; SLEEF

References:

[1]	Abramowitz, M., Stegun, I.A. (eds.): Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables. Wiley, New York (1972) · Zbl 0543.33001
[2]	Akbarpour, B., Paulson, L.: Extending a resolution prover for inequalities on elementary functions. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 47–61 (2007) · Zbl 1137.68571
[3]	Akbarpour, B., Paulson, L.: MetiTarski: an automatic prover for the elementary functions. In: Autexier, S., et al. (eds.) Intelligent Computer Mathematics. LNCS, vol. 5144, pp. 217–231. Springer, New York (2008) · Zbl 1166.68335
[4]	Akbarpour, B., Paulson, L.C.: Towards automatic proofs of inequalities involving elementary functions. In: Cook, B., Sebastiani, R. (eds.): PDPAR: Pragmatics of Decision Procedures in Automated Reasoning, pp. 27–37 (2006)
[5]	Akbarpour, B., Paulson, L.C.: Applications of MetiTarski in the verification of control and hybrid systems. In: Majumdar, R., Tabuada, P. (eds.) Hybrid Systems: Computation and Control. LNCS, vol. 5469, pp. 1–15. Springer, New York (2009) · Zbl 1237.93087
[6]	Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098
[7]	Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 2, pp. 19–99. Elsevier, Amsterdam (2001) · Zbl 0993.03008
[8]	Backeljauw, F., Becuwe, S., Colman, M., Cuyt, A., Docx, T.: Special functions: continued fraction and series representations. http://www.cfhblive.ua.ac.be/ (2008)
[9]	Beeson., M.: Automatic generation of a proof of the irrationality of e. J. Symb. Comput. 32(4), 333–349 (2001) · Zbl 0981.68146
[10]	Bergstra, J.A., Tucker, J.V.: The rational numbers as an abstract data type. J. ACM 54(2), Article No. 7 (2007) · Zbl 1292.68105
[11]	Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97–108 (2003) · Zbl 1083.68148
[12]	Bullen, P.S.: A Dictionary of Inequalities. Longman, New York (1998) · Zbl 0934.26003
[13]	Clarke, E., Zhao, X.: Analytica: a theorem prover for mathematica. Math. J. 3(1), 56–71 (1993)
[14]	Cuyt, A., Petersen, V., Verdonk, B., Waadeland, H., Jones, W.: Handbook of Continued Fractions for Special Functions. Springer, New York (2008) · Zbl 1150.30003
[15]	Cuyt, A.A.M.: Upper/lower bounds (2008). E-mail dated 7 September 2008
[16]	Cuyt, A.A.M., Verdonk, B., Waadeland, H.: Efficient and reliable multiprecision implementation of elementary and special functions. SIAM J. Sci. Comput. 28(4), 1437–1462 (2006) · Zbl 1132.33342
[17]	Daumas, M., Muñoz, C., Lester, D.: Verified real number calculations: a library for integer arithmetic. IEEE Trans. Comput. 58(2), 226–237 (2009) · Zbl 1367.65213
[18]	Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.C.: Automated formal verification of analog designs using MetiTarski. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design (2009)
[19]	Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. Technical report MIP-9720, Universität Passau, D-94030, Germany (1997) · Zbl 0934.68130
[20]	Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1, 209–236 (2007) · Zbl 1144.68371
[21]	Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Preprint (2007) · Zbl 1298.68252
[22]	Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics: TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, New York (2005) · Zbl 1152.68702
[23]	Hardy, R.: Formal methods for control engineering: a validated decision procedure for Nichols plot analysis. Ph.D. thesis, University of St Andrews (2006)
[24]	Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009) · Zbl 1178.03001
[25]	Herde, C.: HySAT Quick Start Guide. University of Oldenburg. http://hysat.informatik.uni-oldenburg.de/user_guide/hysat-user-guide.pdf (2008)
[26]	Hong, H.: QEPCAD–quantifier elimination by partial cylindrical algebraic decomposition. http://www.cs.usna.edu/\(\sim\)qepcad/B/QEPCAD.html (2008)
[27]	Hörmander, L.: The Analysis of Linear Partial Differential Operators II: Differential Operators with Constant Coefficient. Springer, New York (2006) (First published in 1983; cited by McLaughlin and Harrison [34]) · Zbl 0521.35002
[28]	Hurd, J.: Metis first order prover. http://gilith.com/software/metis/ (2007)
[29]	Kaczor, W.J., Nowak, M.T.: Problems in Mathematical Analysis II: Continuity and Differentiation. American Mathematical Society, Providence (2001) · Zbl 0969.00006
[30]	Korovkin, P.P.: Inequalities. Pergamon, Oxford (1961) · Zbl 0108.26904
[31]	Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001) · Zbl 0983.93004
[32]	Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007. Lecture Notes in Computer Science, vol. 4790, pp. 348–362. Springer, New York (2007) · Zbl 1137.03306
[33]	McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997) · Zbl 05468574
[34]	McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction–CADE-20 International Conference. LNAI, vol. 3632, pp. 295–314. Springer, New York (2005) · Zbl 1135.03329
[35]	Mitrinović, D.S., Vasić, P.M.: Analytic Inequalities. Springer, New York (1970) · Zbl 0213.22303
[36]	Muller, J.M.: Elementary Functions: Algorithms and Implementation, 2nd edn. Birkhäuser, Boston (2006) · Zbl 1089.65016
[37]	Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003) · Zbl 1043.14018
[38]	Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC’06 Workshop on Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, pp. 18–33 (2006)
[39]	Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7(4), 723–748 (2006)
[40]	Ratschan, S.: RSolver user manual. Academy of Sciences of the Czech Republic. http://rsolver.sourceforge.net/documentation/manual.pdf (2007)
[41]	Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement ACM Trans. Embed. Comput. Syst. 6(1) (2007) · Zbl 1078.93508
[42]	Ratschan, S., She, Z.: Benchmarks for safety verification of hybrid systems. http://hsolver.sourceforge.net/benchmarks/ (2008) · Zbl 1078.93508
[43]	Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, number 112, pp. 201–215. IOS, Amsterdam (2004)