Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Abramowitz, M., Stegun, I.A. (eds.): Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables. Wiley, New York (1972)
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)
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)
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)
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)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
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)
Backeljauw, F., Becuwe, S., Colman, M., Cuyt, A., Docx, T.: Special functions: continued fraction and series representations. http://www.cfhblive.ua.ac.be/ (2008)
Beeson., M.: Automatic generation of a proof of the irrationality of e. J. Symb. Comput. 32(4), 333–349 (2001)
Bergstra, J.A., Tucker, J.V.: The rational numbers as an abstract data type. J. ACM 54(2), Article No. 7 (2007)
Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97–108 (2003)
Bullen, P.S.: A Dictionary of Inequalities. Longman, New York (1998)
Clarke, E., Zhao, X.: Analytica: a theorem prover for mathematica. Math. J. 3(1), 56–71 (1993)
Cuyt, A., Petersen, V., Verdonk, B., Waadeland, H., Jones, W.: Handbook of Continued Fractions for Special Functions. Springer, New York (2008)
Cuyt, A.A.M.: Upper/lower bounds (2008). E-mail dated 7 September 2008
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)
Daumas, M., Muñoz, C., Lester, D.: Verified real number calculations: a library for integer arithmetic. IEEE Trans. Comput. 58(2), 226–237 (2009)
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)
Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. Technical report MIP-9720, Universität Passau, D-94030, Germany (1997)
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)
Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Preprint (2007)
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)
Hardy, R.: Formal methods for control engineering: a validated decision procedure for Nichols plot analysis. Ph.D. thesis, University of St Andrews (2006)
Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)
Herde, C.: HySAT Quick Start Guide. University of Oldenburg. http://hysat.informatik.uni-oldenburg.de/user_guide/hysat-user-guide.pdf (2008)
Hong, H.: QEPCAD—quantifier elimination by partial cylindrical algebraic decomposition. http://www.cs.usna.edu/~qepcad/B/QEPCAD.html (2008)
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])
Hurd, J.: Metis first order prover. http://gilith.com/software/metis/ (2007)
Kaczor, W.J., Nowak, M.T.: Problems in Mathematical Analysis II: Continuity and Differentiation. American Mathematical Society, Providence (2001)
Korovkin, P.P.: Inequalities. Pergamon, Oxford (1961)
Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001)
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)
McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997)
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)
Mitrinović, D.S., Vasić, P.M.: Analytic Inequalities. Springer, New York (1970)
Muller, J.M.: Elementary Functions: Algorithms and Implementation, 2nd edn. Birkhäuser, Boston (2006)
Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)
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)
Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7(4), 723–748 (2006)
Ratschan, S.: RSolver user manual. Academy of Sciences of the Czech Republic. http://rsolver.sourceforge.net/documentation/manual.pdf (2007)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement ACM Trans. Embed. Comput. Syst. 6(1) (2007)
Ratschan, S., She, Z.: Benchmarks for safety verification of hybrid systems. http://hsolver.sourceforge.net/benchmarks/ (2008)
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)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Akbarpour, B., Paulson, L.C. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J Autom Reasoning 44, 175–205 (2010). https://doi.org/10.1007/s10817-009-9149-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9149-2