MetiTarski swMATH ID: 573 Software Authors: Akbarpour, Behzad; Paulson, Lawrence C. Description: Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure (QEPCAD) for the theory of real closed fields. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic facts, while deleting as redundant clauses that follow algebraically from other clauses. MetiTarski includes special code to simplify arithmetic expressions. Homepage: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-January/msg00109.html Related Software: QEPCAD; z3; PVS; Coq; HOL Light; Isabelle/HOL; KeYmaera; OTTER; Maple; RSOLVER; Flyspeck; HOL; dReal; SPASS+T; ProjectionCAD; RegularChains; SMT-LIB; TPTP; Isabelle; Sledgehammer Cited in: 52 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year MetiTarski: An automatic prover for the elementary functions. Zbl 1166.68335Akbarpour, Behzad; Paulson, Lawrence C. 2008 all top 5 Cited by 91 Authors 11 Paulson, Lawrence Charles 9 England, Matthew 8 Davenport, James Harold 5 Wilson, David J. 4 Bradford, Russell J. 4 Urban, Josef 3 Akbarpour, Behzad 3 Bridge, James P. 3 Kaliszyk, Cezary 3 Passmore, Grant Olney 2 Allamigeon, Xavier 2 Avigad, Jeremy 2 Gaubert, Stéphane 2 Huang, Zongyan 2 Lewis, Robert Y. 2 Magron, Victor 2 Matringe, Nadir 2 Mitsch, Stefan 2 Moura, Arnaldo Vieira 2 Muñoz, César A. 2 Narkawicz, Anthony Joseph 2 Platzer, André 2 Rebiha, Rachid 2 Roux, Cody 2 Sogokon, Andrew 2 Tan, Yong Kiam 2 Werner, Benjamin 1 Abbasi, Rosa 1 Ábrahám, Erika 1 Ahrendt, Wolfgang 1 Alviano, Mario 1 Anai, Hirokazu 1 Arai, Noriko H. 1 Carter, Rebekah 1 Chen, Changbo 1 Chvalovský, Karel 1 Cordwell, Katherine 1 Corzilius, Florian 1 Darulova, Eva 1 de Moura, Leonardo 1 Duracz, Jan 1 Dutle, Aaron 1 Eraşcu, Mădălina 1 Florescu, Dorian 1 Franek, Peter 1 Fukasaku, Ryoya 1 Gallicchio, James 1 Gilbert, Frédéric 1 Gottliebsen, Hanne 1 Hardy, Ruth 1 Hong, Hoon 1 Huang, Chengchao 1 Iwane, Hidenao 1 Jackson, Paul B. 1 Jakubův, Jan 1 Johnson, Taylor T. 1 Junges, Sebastian 1 Kalachev, Gleb V. 1 Kobayashi, Munehiro 1 Konečný, Michal 1 Kovács, Laura Ildikó 1 Kremer, Gereon 1 Kudo, Jumma 1 Kumar, Ramana 1 Kunčar, Ondřej 1 Li, Wenda 1 Li, Zhibin 1 Lightfoot, Olga 1 Lincoln, Patrick D. 1 Martin-Dorel, Érik 1 Martin, Ursula 1 Matsuzaki, Takuya 1 McCallum, Scott 1 Melquiond, Guillaume 1 Moreno Maza, Marc 1 Moser, Georg 1 Navarro-López, Eva María 1 Noschinski, Lars 1 Olšák, Miroslav 1 Peñaloza, Rafael 1 Ratschan, Stefan 1 Sadov, Sergey Yu. 1 Schiffl, Jonas 1 Schupp, Stefan 1 Tiwari, Ashish Kumar 1 Ulbrich, Mattias 1 Voronkov, Andrei 1 Weber, Tjark 1 Xu, Ming 1 Zgliczyński, Piotr 1 Zhan, Yiyang all top 5 Cited in 11 Serials 11 Journal of Automated Reasoning 3 Journal of Symbolic Computation 3 Mathematics in Computer Science 2 Theoretical Computer Science 2 Formal Methods in System Design 1 Mathematical Notes 1 Formal Aspects of Computing 1 AI Communications 1 Annals of Mathematics and Artificial Intelligence 1 Theory and Practice of Logic Programming 1 Journal of Formalized Reasoning all top 5 Cited in 15 Fields 49 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 7 Numerical analysis (65-XX) 5 Systems theory; control (93-XX) 4 Algebraic geometry (14-XX) 3 Operations research, mathematical programming (90-XX) 2 Commutative algebra (13-XX) 2 Real functions (26-XX) 2 Ordinary differential equations (34-XX) 1 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Approximations and expansions (41-XX) Citations by Year