A Quantifier Elimination Algorithm for Linear Real Arithmetic
From MaRDI portal
Publication:5505558
DOI10.1007/978-3-540-89439-1_18zbMATH Open1182.68213arXiv0803.1575OpenAlexW1862725884MaRDI QIDQ5505558FDOQ5505558
Authors: David Monniaux 
Publication date: 27 January 2009
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/0803.1575
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
- Title not available (Why is that?)
- Automated Deduction – CADE-20
- Speeding up the constraint-based method in difference logic
- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
- Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
- Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
- Proof synthesis and reflection for linear arithmetic
- Modular inference of subprogram contracts for safety checking
- Verification Modulo theories
- Sum of squares certificates for containment of \(\mathcal{H}\)-polytopes in \(\mathcal{V}\)-polytopes
- 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
- Qualitative theorem proving in linear constraints
- Local quantifier elimination
- Weak quantifier elimination for the full linear theory of the integers
- Real quantifier elimination is doubly exponential
- Improving strategies via SMT solving
- Linear quantifier elimination as an abstract decision procedure
- Fast approximations of quantifier elimination
- Estimation of the dimensions of some Kisin varieties
- An incremental algorithm for DLO quantifier elimination via constraint propagation
- Solving strong controllability of temporal problems with uncertainty using SMT
- Linear quantifier elimination
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)
