Effective Quantifier Elimination for Presburger Arithmetic with Infinity

DOI10.1007/978-3-642-04103-7_18zbMath1260.68482OpenAlexW1851760673MaRDI 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

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) First-order arithmetic and fragments (03F30) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (2)

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

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

This page was built for publication: Effective Quantifier Elimination for Presburger Arithmetic with Infinity