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.

References in zbMATH (referenced in 26 articles , 1 standard article )

Showing results 1 to 20 of 26.
Sorted by year (citations)

1 2 next

  1. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  2. Bradford, Russell; Davenport, James H.; England, Matthew; McCallum, Scott; Wilson, David: Truth table invariant cylindrical algebraic decomposition (2016)
  3. Eraşcu, Mădălina; Hong, Hoon: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (2016)
  4. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  5. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  6. 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)
  7. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  8. Muñoz, César A.: Formal methods in air traffic management: the case of unmanned aircraft systems (invited lecture) (2015)
  9. 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)
  10. Passmore, Grant Olney: Decidability of univariate real algebra with predicates for rational and integer powers (2015)
  11. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  12. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  13. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
  14. Wilson, D.J.; Bradford, R.J.; Davenport, J.H.; England, M.: Cylindrical algebraic sub-decompositions (2014)
  15. Allamigeon, Xavier; Gaubert, Stéphane; Magron, Victor; Werner, Benjamin: Certification of bounds of non-linear functions: the templates method (2013)
  16. Bridge, James P.; Paulson, Lawrence Charles: Case splitting in an automatic theorem prover for real-valued special functions (2013)
  17. Gottliebsen, Hanne; Hardy, Ruth; Lightfoot, Olga; Martin, Ursula: Applications of real number theorem proving in PVS (2013)
  18. Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL light (2013)
  19. Muñoz, César; Narkawicz, Anthony: Formalization of Bernstein polynomials and applications to global optimization (2013)
  20. Paulson, Lawrence C.: MetiTarski: past and future (2012)

1 2 next