Effective Quantifier Elimination for Presburger Arithmetic with Infinity

DOI10.1007/978-3-642-04103-7_18zbMath1260.68482MaRDI QIDQ3644100

Aless Lasaruk, Thomas Sturm

Publication date: 10 November 2009

Published in: Computer Algebra in Scientific Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04103-7_18

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

68W30: Symbolic computation and algebraic computation

03F30: First-order arithmetic and fragments

03C10: Quantifier elimination, model completeness, and related topics

Related Items

Certified Reasoning with Infinity, Linear Quantifier Elimination as an Abstract Decision Procedure

Uses Software

• REDLOG

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology
• Quantifier elimination for real algebra -- the quadratic case and beyond
• The complexity of almost linear diophantine problems
• Deciding Boolean algebra with Presburger arithmetic
• Weak quantifier elimination for the full linear theory of the integers
• The complexity of linear problems in fields
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• 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
• Weak Integer Quantifier Elimination Beyond the Linear Case
• Automated Deduction – CADE-20
• Presburger arithmetic with bounded quantifier alternation
• Advances in Databases and Information Systems