A heuristic prover for real inequalities

DOI10.1007/978-3-319-08970-6_5zbMATH Open1416.68149OpenAlexW2504213494MaRDI QIDQ2879243FDOQ2879243

Authors: Jeremy Avigad, Robert Y. Lewis, Cody Roux 

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_5

Recommendations

• A heuristic prover for real inequalities
• Extending a Resolution Prover for Inequalities on Elementary Functions
• MetiTarski: An Automatic Prover for the Elementary Functions
• Real Algebraic Strategies for MetiTarski Proofs
• A heuristic prover for elementary analysis in \textit{Theorema}

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited In (3)

• AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
• Extending a Resolution Prover for Inequalities on Elementary Functions
• A heuristic prover for real inequalities

Uses Software

• MetiTarski
• Isabelle/HOL
• SPASS+T
• lrs
• z3
• HOL Light
• Sledgehammer

This page was built for publication: A heuristic prover for real inequalities

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879243)