{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T09:58:26Z","timestamp":1760608706716,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_1","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"1-10","source":"Crossref","is-referenced-by-count":23,"title":["MetiTarski: Past and Future"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Abramowitz, M., Stegun, I.A. (eds.): Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables. Wiley (1972)"},{"key":"1_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-75560-9_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Akbarpour","year":"2007","unstructured":"Akbarpour, B., Paulson, L.C.: Extending a Resolution Prover for Inequalities on Elementary Functions. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 47\u201361. Springer, Heidelberg (2007)"},{"key":"1_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-540-85110-3_18","volume-title":"Intelligent Computer Mathematics","author":"B. Akbarpour","year":"2008","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An Automatic Prover for the Elementary Functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 217\u2013231. Springer, Heidelberg (2008)"},{"issue":"3","key":"1_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR5","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":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00602-9_1","volume-title":"Hybrid Systems: Computation and Control","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.) HSCC 2009. LNCS, vol.\u00a05469, pp. 1\u201315. Springer, Heidelberg (2009)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297660"},{"issue":"4","key":"1_CR8","first-page":"333","volume":"32","author":"M. Beeson","year":"2001","unstructured":"Beeson, M.: Automatic generation of a proof of the irrationality of e. JSC\u00a032(4), 333\u2013349 (2001)","journal-title":"JSC"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence\u00a09, 1\u201335 (1977)","journal-title":"Artificial Intelligence"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Bridge, J., Paulson, L.C.: Case splitting in an automatic theorem prover for real-valued special functions. Journal of Automated Reasoning (in press, 2012), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/s10817-012-9245-6","DOI":"10.1007\/s10817-012-9245-6"},{"issue":"4","key":"1_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"C.W. Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin\u00a037(4), 97\u2013108 (2003)","journal-title":"SIGSAM Bulletin"},{"key":"1_CR13","unstructured":"Bullen, P.S.: A Dictionary of Inequalities. Longman (1998)"},{"issue":"1","key":"1_CR14","first-page":"56","volume":"3","author":"E. Clarke","year":"1993","unstructured":"Clarke, E., Zhao, X.: Analytica: A theorem prover for Mathematica. Mathematica Journal\u00a03(1), 56\u201371 (1993)","journal-title":"Mathematica Journal"},{"key":"1_CR15","unstructured":"Cuyt, A., Petersen, V., Verdonk, B., Waadeland, H., Jones, W.B.: Handbook of Continued Fractions for Special Functions. Springer (2008)"},{"issue":"2","key":"1_CR16","doi-asserted-by":"publisher","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. Computers\u00a058(2), 226\u2013237 (2009)","journal-title":"IEEE Trans. Computers"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbolic Comp.\u00a05, 29\u201335 (1988)","journal-title":"J. Symbolic Comp."},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.C.: Formal verification of analog designs using MetiTarski. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design, pp. 93\u2013100. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351136"},{"issue":"1","key":"1_CR20","doi-asserted-by":"publisher","first-page":"7","DOI":"10.2307\/2274424","volume":"53","author":"L. Dries van den","year":"1988","unstructured":"van den Dries, L.: Alfred Tarski\u2019s elimination theory for real closed fields. The Journal of Symbolic Logic\u00a053(1), 7\u201319 (1988)","journal-title":"The Journal of Symbolic Logic"},{"key":"1_CR21","unstructured":"Hardy, R.: Formal Methods for Control Engineering: A Validated Decision Procedure for Nichols Plot Analysis. PhD thesis, University of St Andrews (2006)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying Nonlinear Real Formulas Via Sums of Squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 102\u2013118. Springer, Heidelberg (2007)"},{"key":"1_CR23","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (September 2003)"},{"key":"1_CR24","unstructured":"Hurd, J.: Metis first order prover (2007), Website at, \n                    \n                      http:\/\/gilith.com\/software\/metis\/"},{"key":"1_CR25","unstructured":"Jovanovic\u0300, D., de Moura, L.: Solving Non-linear Arithmetic. Technical Report MSR-TR-2012-20, Microsoft Research (2012) (accepted to IJCAR 2012)"},{"issue":"3","key":"1_CR26","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., Maher, M.J.: On Fourier\u2019s algorithm for linear arithmetic constraints. Journal of Automated Reasoning\u00a09(3), 373\u2013379 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A Proof-Producing Decision Procedure for Real Arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Mitrinovi\u0107, D.S., Vasi\u0107, P.M.: Analytic Inequalities. Springer (1970)","DOI":"10.1007\/978-3-642-99970-3"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/11541868_13","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Mu\u00f1oz","year":"2005","unstructured":"Mu\u00f1oz, C., Lester, D.R.: Real Number Calculations and Theorem Proving. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 195\u2013210. Springer, Heidelberg (2005)"},{"key":"1_CR30","unstructured":"Passmore, G.O., Paulson, L.C., de Moura, L.: Real algebraic strategies for MetiTarski proofs. In: Jeuring, J. (ed.) Conferences on Intelligent Computer Mathematics, CICM 2012. Springer (in press, 2012)"},{"issue":"1","key":"1_CR31","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Logic Computation\u00a020(1), 309\u2013352 (2010)","journal-title":"J. Logic Computation"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"1_CR33","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"issue":"4","key":"1_CR34","doi-asserted-by":"publisher","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. Logic\u00a07(4), 723\u2013748 (2006)","journal-title":"ACM Trans. Comput. Logic"},{"key":"1_CR35","unstructured":"Ratschan, S., She, Z.: Benchmarks for safety verification of hybrid systems (2008), \n                    \n                      http:\/\/hsolver.sourceforge.net\/benchmarks\/"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:01:01Z","timestamp":1620129661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}