A Quantifier Elimination Algorithm for Linear Real Arithmetic
From MaRDI portal
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
(35)- Real quantifier elimination is doubly exponential
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Solving strong controllability of temporal problems with uncertainty using SMT
- A layered algorithm for quantifier elimination from linear modular constraints
- Solving linear constraints over real and rational fields
- Out of order quantifier elimination for standard quantified linear programs
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Sum of squares certificates for containment of \(\mathcal{H}\)-polytopes in \(\mathcal{V}\)-polytopes
- Speeding up the constraint-based method in difference logic
- A survey of satisfiability modulo theory
- Quantifier elimination for linear modular constraints
- Adapting real quantifier elimination methods for conflict set computation
- Improving strategies via SMT solving
- Applying Linear Quantifier Elimination
- No need knowing numerous neighbours. Towards a realizable interpretation of MLSL
- Local quantifier elimination
- Verifying Mixed Real-Integer Quantifier Elimination
- scientific article; zbMATH DE number 1490034 (Why is no real title available?)
- Estimation of the dimensions of some Kisin varieties
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Qualitative theorem proving in linear constraints
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Automated Deduction – CADE-20
- Computer Algebra in Scientific Computing
- Linear quantifier elimination as an abstract decision procedure
- Modular inference of subprogram contracts for safety checking
- Verification Modulo theories
- Fast approximations of quantifier elimination
- Inner and outer approximations of arbitrarily quantified reachability problems
- Linear quantifier elimination
- An incremental algorithm for DLO quantifier elimination via constraint propagation
- Causality-based game solving
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- Weak quantifier elimination for the full linear theory of the integers
- Proof synthesis and reflection for linear arithmetic
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)
