Applying Linear Quantifier Elimination

From MaRDI portal
Publication:3140556

DOI10.1093/comjnl/36.5.450zbMath0787.03021OpenAlexW2013702670MaRDI QIDQ3140556

Volker Weispfenning, Rüdiger Loos

Publication date: 23 May 1994

Published in: The Computer Journal (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/comjnl/36.5.450



Related Items

A layered algorithm for quantifier elimination from linear modular constraints, A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Parametric toricity of steady state varieties of reaction networks, Applied Algebraic Geometry in Model Based Design for Manufacturing, A decision procedure for linear ``big O equations, A quantifier-elimination based heuristic for automatically generating inductive assertions for programs, An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, Verification Modulo theories, An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, New techniques for linear arithmetic: cubes and equalities, Solving quantified linear arithmetic by counterexample-guided instantiation, Better answers to real questions, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications, Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, Unnamed Item, Fast theorem-proving and Wu's method, Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract), Unnamed Item, Cylindrical algebraic decomposition using validated numerics, Quantifier elimination in automatic loop parallelization, Multiple object semilinear motion planning, Syntax-guided quantifier instantiation, On a decision procedure for quantified linear programs, Weak quantifier elimination for the full linear theory of the integers, Solving and visualizing nonlinear parametric constraints in control based on quantifier elimination, Proof synthesis and reflection for linear arithmetic, SMT-based model checking for recursive programs, Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants, Automatic generation of bounds for polynomial systems with application to the Lorenz system, Classical numerical methods in engineering: a note on existential quantifier elimination under parametric inequality constraints, Linear quantifier elimination, Linear Quantifier Elimination as an Abstract Decision Procedure, Improved algorithms for linear complementarity problem arising from collision response, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Identifying the parametric occurrence of multiple steady states for some biological networks, Cylindrical algebraic decomposition using local projections, Certified Reasoning with Infinity, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, On solving quantified bit-vector constraints using invertibility conditions, Combining logical and algebraic techniques for natural style proving in elementary analysis, Effective Quantifier Elimination for Presburger Arithmetic with Infinity, Don't care words with an application to the automata-based approach for real addition, A Survey of Satisfiability Modulo Theory, Automatic derivation of positivity conditions inside boundary elements with the help of the REDLOG computer logic package., Quantifier elimination for trigonometric polynomials by cylindrical trigonometric decomposition, Linear problems in valued fields, 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, Solving strong controllability of temporal problems with uncertainty using SMT, Symbolic model checking of timed guarded commands using difference decision diagrams, Survey on mining signal temporal logic specifications, Quantified constraints under perturbation