Weak quantifier elimination for the full linear theory of the integers

DOI10.1007/s00200-007-0053-xzbMath1154.68112OpenAlexW2097821910MaRDI QIDQ945000

Thomas Sturm, Aless Lasaruk

Publication date: 10 September 2008

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00200-007-0053-x

zbMATH Keywords

quantifier eliminationimplementationinteger constraint solving

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies ⋮ Linear Integer Arithmetic Revisited ⋮ Detection of Hopf bifurcations in chemical reaction networks using convex coordinates ⋮ Bounding quantification in parametric expansions of Presburger arithmetic ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ Better answers to real questions ⋮ Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior ⋮ Algorithmic global criteria for excluding oscillations ⋮ Parametric Qualitative Analysis of Ordinary Differential Equations: Computer Algebra Methods for Excluding Oscillations (Extended Abstract) (Invited Talk) ⋮ A complete and terminating approach to linear integer solving ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity

Uses Software

• REDUCE
• REDLOG

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quantifier elimination for real algebra -- the quadratic case and beyond
• The complexity of almost linear diophantine problems
• Conditions for the existence of solutions of the three-dimensional planar transportation problem
• The complexity of linear problems in fields
• The complexity of logical theories
• The computational complexity of logical theories
• Simulation and optimization by quantifier elimination
• Simplification of quantifier-free formulae over ordered fields
• Linear problems in valued fields
• Applying Linear Quantifier Elimination
• A Decision Procedure for the First Order Theory of Real Addition with Order
• A Bound on Solutions of Linear Integer Equalities and Inequalities
• Hilbert's Tenth Problem is Unsolvable