A Heuristic Prover for Real Inequalities

Reference. A Heuristic Prover for Real Inequalities

Jeremy Avigad, Robert Y. Lewis, Cody Roux · JAR · 2016 · DOI · arXiv

Cite

Cite as @avigad-2016-a (helia, typst) · \cite{avigad-2016-a} (LaTeX)

BibTeX

bibtex · 1 line

@article{avigad-2016-a, title={A Heuristic Prover for Real Inequalities}, volume={56}, ISSN={1573-0670}, url={http://dx.doi.org/10.1007/s10817-015-9356-y}, DOI={10.1007/s10817-015-9356-y}, number={3}, journal={Journal of Automated Reasoning}, publisher={Springer Science and Business Media LLC}, author={Avigad, Jeremy and Lewis, Robert Y. and Roux, Cody}, year={2016}, month=Jan, pages={367–386} }

hayagriva YAML (typst)

yaml · 19 lines

avigad-2016-a:
  type: article
  title: A Heuristic Prover for Real Inequalities
  author:
  - Avigad, Jeremy
  - Lewis, Robert Y.
  - Roux, Cody
  date: 2016-01
  page-range: 367-386
  url: http://dx.doi.org/10.1007/s10817-015-9356-y
  serial-number:
    doi: 10.1007/s10817-015-9356-y
    issn: 1573-0670
  parent:
    type: periodical
    title: Journal of Automated Reasoning
    publisher: Springer Science, Business Media LLC
    issue: 3
    volume: 56

Download: avigad-2016-a.bib · avigad-2016-a.yml

Cites 39 works (0 here)

External (39)

A Formally Verified Proof of the Central Limit Theorem (2017)
A heuristic prover for real inequalities (2014)
Polya: a heuristic procedure for reasoning with real inequalities (M.S. thesis) (2014)
δ-Complete Decision Procedures for Satisfiability over the Reals (2012)
Extending Sledgehammer with SMT solvers (2011)
Satisfiability modulo theories (2009)
Lightweight relevance filtering for machine-generated resolution problems (2009)
Introduction to Interval Analysis (2009)
Real World Verification (2009)
Proof Synthesis and Reflection for Linear Arithmetic (2008)
Z3: An Efficient SMT Solver (2008)
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (2008)
E-matching for Fun and Profit (2008)
MetiTarski: An Automatic Prover for the Elementary Functions (2008)
A formally verified proof of the prime number theorem (2007)
Efficient E-Matching for SMT Solvers (2007)
Inequalities: A Journey into Linear Analysis (2007)
Verifying Nonlinear Real Formulas Via Sums of Squares (2007)
Combining decision procedures for the reals (2006)
A Fast Linear-Arithmetic Solver for DPLL(T) (2006)
A Proof-Producing Decision Procedure for Real Arithmetic (2005)
Convex Optimization (2004)
A Certified AC Matching Algorithm (2004)
Equality Set Projection: A new algorithm for the projection of polytopes in halfspace representation (2004)
Algorithms in Real Algebraic Geometry (2003)
Linear and Nonlinear Arithmetic in ACL2 (2003)
Isabelle/HOL. A Proof Assistant for Higher-Order Logic (2002)
Living with lrs (2000)
Computer-Aided Reasoning: An Approach (2000)
Double Description Method Revisited (1996)
HOL Light: A tutorial introduction (1996)
Probability and Measure (3rd ed.) (1995)
Lectures on Polytopes (1995)
The Omega test: a fast and practical integer programming algorithm for dependence analysis (1991)
Inequalities (Hardy, Littlewood, Pólya; reprint) (1988)
Theory of Linear and Integer Programming (1986)
Simplification by Cooperating Decision Procedures (1979)
Algebraic simplification: a guide for the perplexed (1971)
How to Solve It (1945)