MetiTarski
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.
Keywords for this software
References in zbMATH (referenced in 32 articles , 1 standard article )
Showing results 1 to 20 of 32.
Sorted by year (- Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
- Bradford, Russell; Davenport, James H.; England, Matthew; McCallum, Scott; Wilson, David: Truth table invariant cylindrical algebraic decomposition (2016)
- England, Matthew; Davenport, James H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree (2016)
- Eraşcu, Mădălina; Hong, Hoon: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (2016)
- Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr: Quasi-decidability of a fragment of the first-order theory of real numbers (2016)
- Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
- Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
- Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
- Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving (2015)
- Davenport, James H.; England, Matthew: Recent advances in real geometric reasoning (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Muñoz, César A.: Formal methods in air traffic management: the case of unmanned aircraft systems (invited lecture) (2015)
- Narkawicz, Anthony; Muñoz, César; Dutle, Aaron: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems (2015)
- Passmore, Grant Olney: Decidability of univariate real algebra with predicates for rational and integer powers (2015)
- Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport
- Wilson, D.J.; Bradford, R.J.; Davenport, J.H.; England, M.: Cylindrical algebraic sub-decompositions (2014)
- Allamigeon, Xavier; Gaubert, Stéphane; Magron, Victor; Werner, Benjamin: Certification of bounds of non-linear functions: the templates method (2013)
- Bridge, James P.; Paulson, Lawrence Charles: Case splitting in an automatic theorem prover for real-valued special functions (2013)