A heuristic prover for real inequalities

DOI10.1007/978-3-319-08970-6_5MaRDI QIDQ2879243zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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}

Cited in

(3)

• AUTO2, a saturation-based heuristic prover for higher-order logic
• A heuristic prover for real inequalities
• Extending a Resolution Prover for Inequalities on Elementary Functions

Describes a project that uses

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)