Verifying Mixed Real-Integer Quantifier Elimination
From MaRDI portal
Recommendations
- Verification and synthesis using real quantifier elimination
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Quantifier Elimination and Provers Integration
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Real quantifier elimination in the RegularChains library
- Variant real quantifier elimination: algorithm and application
- scientific article; zbMATH DE number 1302474
- Real quantifier elimination by computation of comprehensive Gröbner systems
- Solving quantified verification conditions using satisfiability modulo theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Cited in
(12)- Don't care words with an application to the automata-based approach for real addition
- Formalization of real analysis: a survey of proof assistants and libraries
- Linear Quantifier Elimination
- Verification and synthesis using real quantifier elimination
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Linear quantifier elimination as an abstract decision procedure
- Verified Quadratic Virtual Substitution for Real Arithmetic
- Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
- Linear quantifier elimination
- Proof synthesis and reflection for linear arithmetic
This page was built for publication: Verifying Mixed Real-Integer Quantifier Elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613432)
