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.


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

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

1 2 3 next

  1. England, Matthew; Bradford, Russell; Davenport, James H.: Cylindrical algebraic decomposition with equational constraints (2020)
  2. Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin: A conflict-driven solving procedure for poly-power constraints (2020)
  3. England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
  4. Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.: Using machine learning to improve cylindrical algebraic decomposition (2019)
  5. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  6. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  7. Kalachev, G. V.; Sadov, S. Yu.: A logarithmic inequality (2018)
  8. Gilbert, Frédéric: Proof certificates in PVS (2017)
  9. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  10. Bradford, Russell; Davenport, James H.; England, Matthew; McCallum, Scott; Wilson, David: Truth table invariant cylindrical algebraic decomposition (2016)
  11. England, Matthew; Davenport, James H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree (2016)
  12. Eraşcu, Mădălina; Hong, Hoon: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (2016)
  13. Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr: Quasi-decidability of a fragment of the first-order theory of real numbers (2016)
  14. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  15. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  16. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)
  17. Alviano, Mario; Peñaloza, Rafael: Fuzzy answer set computation via satisfiability modulo theories (2015)
  18. 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)
  19. Davenport, James H.; England, Matthew: Recent advances in real geometric reasoning (2015)
  20. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)

1 2 3 next