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 44 articles , 1 standard article )
Showing results 1 to 20 of 44.
Sorted by year (- England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
- Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
- Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
- Kalachev, G. V.; Sadov, S. Yu.: A logarithmic inequality (2018)
- Gilbert, Frédéric: Proof certificates in PVS (2017)
- 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)
- Alviano, Mario; Peñaloza, Rafael: Fuzzy answer set computation via satisfiability modulo theories (2015)
- Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: \textttSMT-RAT: an open source \textttC++ 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)