{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T05:25:24Z","timestamp":1789881924444,"version":"4.0.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,8,18]],"date-time":"2009-08-18T00:00:00Z","timestamp":1250553600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s10817-009-9149-2","type":"journal-article","created":{"date-parts":[[2009,8,17]],"date-time":"2009-08-17T07:26:52Z","timestamp":1250494012000},"page":"175-205","source":"Crossref","is-referenced-by-count":84,"title":["MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions"],"prefix":"10.1007","volume":"44","author":[{"given":"Behzad","family":"Akbarpour","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence Charles","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2009,8,18]]},"reference":[{"key":"9149_CR1","volume-title":"Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables","year":"1972","unstructured":"Abramowitz, M., Stegun, I.A. (eds.): Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables. Wiley, New York (1972)"},{"key":"9149_CR2","doi-asserted-by":"crossref","unstructured":"Akbarpour, B., Paulson, L.: Extending a resolution prover for inequalities on elementary functions. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 47\u201361 (2007)","DOI":"10.1007\/978-3-540-75560-9_6"},{"key":"9149_CR3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-540-85110-3_18","volume-title":"Intelligent Computer Mathematics. LNCS, vol.\u00a05144","author":"B Akbarpour","year":"2008","unstructured":"Akbarpour, B., Paulson, L.: MetiTarski: an automatic prover for the elementary functions. In: Autexier, S., et\u00a0al. (eds.) Intelligent Computer Mathematics. LNCS, vol.\u00a05144, pp. 217\u2013231. Springer, New York (2008)"},{"key":"9149_CR4","unstructured":"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\u201337 (2006)"},{"key":"9149_CR5","first-page":"1","volume-title":"Hybrid Systems: Computation and Control. LNCS, vol.\u00a05469","author":"B Akbarpour","year":"2009","unstructured":"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.\u00a05469, pp. 1\u201315. Springer, New York (2009)"},{"key":"9149_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"9149_CR7","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, vol. I, chap.\u00a02","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap.\u00a02, pp.\u00a019\u201399. Elsevier, Amsterdam (2001)"},{"key":"9149_CR8","unstructured":"Backeljauw, F., Becuwe, S., Colman, M., Cuyt, A., Docx, T.: Special functions: continued fraction and series representations. http:\/\/www.cfhblive.ua.ac.be\/ (2008)"},{"issue":"4","key":"9149_CR9","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1006\/jsco.2000.0465","volume":"32","author":"M Beeson.","year":"2001","unstructured":"Beeson., M.: Automatic generation of a proof of the irrationality of e. J. Symb. Comput. 32(4), 333\u2013349 (2001)","journal-title":"J. Symb. Comput."},{"key":"9149_CR10","doi-asserted-by":"crossref","unstructured":"Bergstra, J.A., Tucker, J.V.: The rational numbers as an abstract data type. J. ACM 54(2), Article No.\u00a07 (2007)","DOI":"10.1145\/1219092.1219095"},{"issue":"4","key":"9149_CR11","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97\u2013108 (2003)","journal-title":"SIGSAM Bull."},{"key":"9149_CR12","volume-title":"A Dictionary of Inequalities","author":"PS Bullen","year":"1998","unstructured":"Bullen, P.S.: A Dictionary of Inequalities. Longman, New York (1998)"},{"issue":"1","key":"9149_CR13","first-page":"56","volume":"3","author":"E Clarke","year":"1993","unstructured":"Clarke, E., Zhao, X.: Analytica: a theorem prover for mathematica. Math. J. 3(1), 56\u201371 (1993)","journal-title":"Math. J."},{"key":"9149_CR14","volume-title":"Handbook of Continued Fractions for Special Functions","author":"A Cuyt","year":"2008","unstructured":"Cuyt, A., Petersen, V., Verdonk, B., Waadeland, H., Jones, W.: Handbook of Continued Fractions for Special Functions. Springer, New York (2008)"},{"key":"9149_CR15","unstructured":"Cuyt, A.A.M.: Upper\/lower bounds (2008). E-mail dated 7 September 2008"},{"issue":"4","key":"9149_CR16","doi-asserted-by":"crossref","first-page":"1437","DOI":"10.1137\/050629203","volume":"28","author":"AAM Cuyt","year":"2006","unstructured":"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\u20131462 (2006)","journal-title":"SIAM J. Sci. Comput."},{"issue":"2","key":"9149_CR17","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Mu\u00f1oz, C., Lester, D.: Verified real number calculations: a library for integer arithmetic. IEEE Trans. Comput. 58(2), 226\u2013237 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"9149_CR18","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/FMCAD.2009.5351136"},{"key":"9149_CR19","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. Technical report MIP-9720, Universit\u00e4t Passau, D-94030, Germany (1997)"},{"key":"9149_CR20","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, 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\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9149_CR21","unstructured":"Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Preprint (2007)"},{"key":"9149_CR22","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs 2005. LNCS, vol.\u00a03603","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, 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.\u00a03603, pp.\u00a098\u2013113. Springer, New York (2005)"},{"key":"9149_CR23","unstructured":"Hardy, R.: Formal methods for control engineering: a validated decision procedure for Nichols plot analysis. Ph.D. thesis, University of St Andrews (2006)"},{"key":"9149_CR24","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"9149_CR25","unstructured":"Herde, C.: HySAT Quick Start Guide. University of Oldenburg. http:\/\/hysat.informatik.uni-oldenburg.de\/user_guide\/hysat-user-guide.pdf (2008)"},{"key":"9149_CR26","unstructured":"Hong, H.: QEPCAD\u2014quantifier elimination by partial cylindrical algebraic decomposition. http:\/\/www.cs.usna.edu\/~qepcad\/B\/QEPCAD.html (2008)"},{"key":"9149_CR27","volume-title":"The Analysis of Linear Partial Differential Operators II: Differential Operators with Constant Coefficient","author":"L H\u00f6rmander","year":"2006","unstructured":"H\u00f6rmander, 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\u00a0[34])"},{"key":"9149_CR28","unstructured":"Hurd, J.: Metis first order prover. http:\/\/gilith.com\/software\/metis\/ (2007)"},{"key":"9149_CR29","volume-title":"Problems in Mathematical Analysis II: Continuity and Differentiation.","author":"WJ Kaczor","year":"2001","unstructured":"Kaczor, W.J., Nowak, M.T.: Problems in Mathematical Analysis II: Continuity and Differentiation. American Mathematical Society, Providence (2001)"},{"key":"9149_CR30","volume-title":"Inequalities","author":"PP Korovkin","year":"1961","unstructured":"Korovkin, P.P.: Inequalities. Pergamon, Oxford (1961)"},{"issue":"3","key":"9149_CR31","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231\u2013253 (2001)","journal-title":"J. Symb. Comput."},{"key":"9149_CR32","first-page":"348","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007. Lecture Notes in Computer Science, vol. 4790","author":"M Ludwig","year":"2007","unstructured":"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\u2013362. Springer, New York (2007)"},{"issue":"2","key":"9149_CR33","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W McCune","year":"1997","unstructured":"McCune, W., Wos, L.: Otter: the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997)","journal-title":"J. Autom. Reason."},{"key":"9149_CR34","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction\u2014CADE-20 International Conference. LNAI, vol.\u00a03632","author":"S McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction\u2014CADE-20 International Conference. LNAI, vol.\u00a03632, pp. 295\u2013314. Springer, New York (2005)"},{"key":"9149_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-99970-3","volume-title":"Analytic Inequalities","author":"DS Mitrinovi\u0107","year":"1970","unstructured":"Mitrinovi\u0107, D.S., Vasi\u0107, P.M.: Analytic Inequalities. Springer, New York (1970)"},{"key":"9149_CR36","volume-title":"Elementary Functions: Algorithms and Implementation","author":"JM Muller","year":"2006","unstructured":"Muller, J.M.: Elementary Functions: Algorithms and Implementation, 2nd edn. Birkh\u00e4user, Boston (2006)","edition":"2"},{"issue":"2","key":"9149_CR37","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","journal-title":"Math. Program."},{"key":"9149_CR38","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, pp. 18\u201333 (2006)"},{"issue":"4","key":"9149_CR39","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1145\/1183278.1183282","volume":"7","author":"S Ratschan","year":"2006","unstructured":"Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7(4), 723\u2013748 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"9149_CR40","unstructured":"Ratschan, S.: RSolver user manual. Academy of Sciences of the Czech Republic. http:\/\/rsolver.sourceforge.net\/documentation\/manual.pdf (2007)"},{"key":"9149_CR41","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement ACM Trans. Embed. Comput. Syst. 6(1) (2007)","DOI":"10.1145\/1210268.1210276"},{"key":"9149_CR42","unstructured":"Ratschan, S., She, Z.: Benchmarks for safety verification of hybrid systems. http:\/\/hsolver.sourceforge.net\/benchmarks\/ (2008)"},{"key":"9149_CR43","unstructured":"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\u2013215. IOS, Amsterdam (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9149-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9149-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9149-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T13:25:01Z","timestamp":1590067501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9149-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,18]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["9149"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9149-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8,18]]}}}