Real Algebraic Strategies for MetiTarski Proofs

DOI10.1007/978-3-642-31374-5_24MaRDI QIDQ2907335zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Leonardo de Moura, Grant Olney Passmore, Lawrence C. Paulson

Publication date 7 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-31374-5_24

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1745035
• On the metamathematics of algebra
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• scientific article; zbMATH DE number 3979056
• Methods for algorithmic meta theorems
• Affine arithmetic and applications to real-number proving
• From Coinductive Proofs to Exact Real Arithmetic
• scientific article; zbMATH DE number 1107623
• Algebra of proofs
• Real analysis. With proof strategies

Cited in

(11)

• Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• A heuristic prover for real inequalities
• Extending a Resolution Prover for Inequalities on Elementary Functions
• A heuristic prover for real inequalities
• MetiTarski: An automatic theorem prover for real-valued special functions
• MetiTarski's menagerie of cooperating systems
• Combining logical and algebraic techniques for natural style proving in elementary analysis
• MetiTarski: An Automatic Prover for the Elementary Functions
• MetiTarski: past and future
• An augmented MetiTarski dataset for real quantifier elimination using machine learning

Describes a project that uses

Uses Software

• RealPaver
• QEPCAD
• MetiTarski

This page was built for publication: Real Algebraic Strategies for MetiTarski Proofs

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