Applying Linear Quantifier Elimination
From MaRDI portal
Recommendations
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Quantifier elimination for real algebra -- the quadratic case and beyond
- An effective algorithm for quantifier elimination over algebraically closed fields using straight line programs
- Linear quantifier elimination
- Linear Quantifier Elimination
Cited in
(65)- Symbolic model checking of timed guarded commands using difference decision diagrams
- The QSMA algorithm for quantifiers in SMT
- Survey on mining signal temporal logic specifications
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Parametric toricity of steady state varieties of reaction networks
- Better answers to real questions
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Towards incorporating background theories into quantifier elimination
- Improved algorithms for linear complementarity problem arising from collision response
- Effective Quantifier Elimination for Presburger Arithmetic with Infinity
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- FMplex: exploring a bridge between Fourier-Motzkin and simplex
- A decision procedure for linear ``big O equations
- Out of order quantifier elimination for standard quantified linear programs
- Syntax-guided quantifier instantiation
- On solving quantified bit-vector constraints using invertibility conditions
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Dines-Fourier-Motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields
- Multiple object semilinear motion planning
- Quantified constraints under perturbation
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- Automatic generation of bounds for polynomial systems with application to the Lorenz system
- An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
- Applied Algebraic Geometry in Model Based Design for Manufacturing
- VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
- Identifying the parametric occurrence of multiple steady states for some biological networks
- Classical numerical methods in engineering: a note on existential quantifier elimination under parametric inequality constraints
- Proof synthesis and reflection for linear arithmetic
- Don't care words with an application to the automata-based approach for real addition
- Cylindrical algebraic decomposition using validated numerics
- Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach
- Discussion on: ``Stabilisability and stability for explicit and implicit polynomial systems: A symbolic computation approach by D. Nešić and I. M. Y. Mareels
- On a decision procedure for quantified linear programs
- Verification Modulo theories
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- Combining logical and algebraic techniques for natural style proving in elementary analysis
- Quantifier elimination in automatic loop parallelization
- A survey of satisfiability modulo theory
- scientific article; zbMATH DE number 1507955 (Why is no real title available?)
- scientific article; zbMATH DE number 1684364 (Why is no real title available?)
- SMT solving for functional programming over infinite structures
- Linear problems in valued fields
- Computer Algebra in Scientific Computing
- A layered algorithm for quantifier elimination from linear modular constraints
- Quantifier elimination and Craig interpolation: the quantitative way
- New techniques for linear arithmetic: cubes and equalities
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Weak quantifier elimination for the full linear theory of the integers
- Local quantifier elimination
- Automatic derivation of positivity conditions inside boundary elements with the help of the REDLOG computer logic package.
- Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract)
- Solving and visualizing nonlinear parametric constraints in control based on quantifier elimination
- Fast theorem-proving and Wu's method
- Linear quantifier elimination as an abstract decision procedure
- Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition
- SMT-based model checking for recursive programs
- Cylindrical algebraic decomposition using local projections
- Linear quantifier elimination
- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
- Solving strong controllability of temporal problems with uncertainty using SMT
- FMplex: a novel method for solving linear real arithmetic problems
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- Certified reasoning with infinity
This page was built for publication: Applying Linear Quantifier Elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3140556)
