A Quantifier Elimination Algorithm for Linear Real Arithmetic
From MaRDI portal
Publication:5505558
Abstract: We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily.
Recommendations
- An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
- Variant real quantifier elimination: algorithm and application
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- Linear quantifier elimination
- Linear Quantifier Elimination
- Quantifier elimination for real algebra -- the quadratic case and beyond
- An effective decision procedure for linear arithmetic over the integers and reals
- Real quantifier elimination by computation of comprehensive Gröbner systems
- Verifying Mixed Real-Integer Quantifier Elimination
Cited in
(34)- Causality-based game solving
- Adapting real quantifier elimination methods for conflict set computation
- Computer Algebra in Scientific Computing
- Out of order quantifier elimination for standard quantified linear programs
- scientific article; zbMATH DE number 1490034 (Why is no real title available?)
- Automated Deduction – CADE-20
- Speeding up the constraint-based method in difference logic
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Proof synthesis and reflection for linear arithmetic
- Modular inference of subprogram contracts for safety checking
- Sum of squares certificates for containment of \(\mathcal{H}\)-polytopes in \(\mathcal{V}\)-polytopes
- Verification Modulo theories
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- Applying Linear Quantifier Elimination
- No need knowing numerous neighbours. Towards a realizable interpretation of MLSL
- A survey of satisfiability modulo theory
- Solving linear constraints over real and rational fields
- A layered algorithm for quantifier elimination from linear modular constraints
- Quantifier elimination for linear modular constraints
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Verifying Mixed Real-Integer Quantifier Elimination
- Weak quantifier elimination for the full linear theory of the integers
- Qualitative theorem proving in linear constraints
- Local quantifier elimination
- Real quantifier elimination is doubly exponential
- Improving strategies via SMT solving
- Linear quantifier elimination as an abstract decision procedure
- Estimation of the dimensions of some Kisin varieties
- Fast approximations of quantifier elimination
- An incremental algorithm for DLO quantifier elimination via constraint propagation
- Linear quantifier elimination
- Solving strong controllability of temporal problems with uncertainty using SMT
This page was built for publication: A Quantifier Elimination Algorithm for Linear Real Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505558)
