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 54 articles , 1 standard article )

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

1 2 3 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Learning theorem proving components (2021)
  3. Sogokon, Andrew; Mitsch, Stefan; Tan, Yong Kiam; Cordwell, Katherine; Platzer, André: Pegasus: sound continuous invariant generation (2021)
  4. England, Matthew; Bradford, Russell; Davenport, James H.: Cylindrical algebraic decomposition with equational constraints (2020)
  5. Huang, Cheng-Chao; Xu, Ming; Li, Zhi-Bin: A conflict-driven solving procedure for poly-power constraints (2020)
  6. England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
  7. Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.: Using machine learning to improve cylindrical algebraic decomposition (2019)
  8. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  9. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  10. Kalachev, G. V.; Sadov, S. Yu.: A logarithmic inequality (2018)
  11. Matsuzaki, Takuya; Iwane, Hidenao; Kobayashi, Munehiro; Zhan, Yiyang; Fukasaku, Ryoya; Kudo, Jumma; Anai, Hirokazu; Arai, Noriko H.: Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems (2018)
  12. Gilbert, Frédéric: Proof certificates in PVS (2017)
  13. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  14. Bradford, Russell; Davenport, James H.; England, Matthew; McCallum, Scott; Wilson, David: Truth table invariant cylindrical algebraic decomposition (2016)
  15. England, Matthew; Davenport, James H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree (2016)
  16. Eraşcu, Mădălina; Hong, Hoon: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (2016)
  17. Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr: Quasi-decidability of a fragment of the first-order theory of real numbers (2016)
  18. Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
  19. Navarro-López, Eva M.; Carter, Rebekah: Deadness and how to disprove liveness in hybrid dynamical systems (2016)
  20. Tiwari, Ashish; Lincoln, Patrick: A search-based procedure for nonlinear real arithmetic (2016)

1 2 3 next