Real Algebraic Strategies for MetiTarski Proofs
From MaRDI portal
Publication:2907335
DOI10.1007/978-3-642-31374-5_24zbMATH Open1360.68764DBLPconf/aisc/PassmorePM12OpenAlexW1492057809WikidataQ57382600 ScholiaQ57382600MaRDI QIDQ2907335FDOQ2907335
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
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
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- A heuristic prover for real inequalities
- 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
Uses Software
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)
