A heuristic prover for real inequalities
From MaRDI portal
Publication:287379
DOI10.1007/s10817-015-9356-yzbMath1356.68174arXiv1404.4410OpenAlexW1564066985MaRDI QIDQ287379
Jeremy Avigad, Robert Y. Lewis, Cody Roux
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1404.4410
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Verified interactive computation of definite integrals
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proof synthesis and reflection for linear arithmetic
- Lightweight relevance filtering for machine-generated resolution problems
- Isabelle/HOL. A proof assistant for higher-order logic
- A formally verified proof of the central limit theorem
- E-matching for Fun and Profit
- A Heuristic Prover for Real Inequalities
- δ-Complete Decision Procedures for Satisfiability over the Reals
- Verifying Nonlinear Real Formulas Via Sums of Squares
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Introduction to Interval Analysis
- Efficient E-Matching for SMT Solvers
- Simplification by Cooperating Decision Procedures
- Lectures on Polytopes
- Real World Verification
- Extending Sledgehammer with SMT Solvers
- A formally verified proof of the prime number theorem
- Combining decision procedures for the reals
- Automated Deduction – CADE-20
- MetiTarski: An Automatic Prover for the Elementary Functions
- Algebraic simplification
- Correct Hardware Design and Verification Methods
- Rewriting Techniques and Applications
- Algorithms in real algebraic geometry
This page was built for publication: A heuristic prover for real inequalities
