Effective Quantifier Elimination for Presburger Arithmetic with Infinity

DOI10.1007/978-3-642-04103-7_18MaRDI QIDQ3644100zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 1253963
• On Presburger arithmetic extended with modulo counting quantifiers
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• Presburger arithmetic with bounded quantifier alternation
• scientific article; zbMATH DE number 1979549

Cites work

• scientific article; zbMATH DE number 3501006 (Why is no real title available?)
• scientific article; zbMATH DE number 3550662 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Advances in Databases and Information Systems
• Applying Linear Quantifier Elimination
• Automated Deduction – CADE-20
• Deciding Boolean algebra with Presburger arithmetic
• Investigating algebraic and logical algorithms to solve Hopf bifurcation problems in algebraic biology
• Linear problems in valued fields
• Presburger arithmetic with bounded quantifier alternation
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Simplification of quantifier-free formulae over ordered fields
• Simulation and optimization by quantifier elimination
• The complexity of almost linear diophantine problems
• The complexity of linear problems in fields
• The computational complexity of logical theories
• Weak Integer Quantifier Elimination Beyond the Linear Case
• Weak quantifier elimination for the full linear theory of the integers

Cited in

(5)

• Quantifier elimination for counting extensions of Presburger arithmetic
• Presburger arithmetic with bounded quantifier alternation
• On Presburger arithmetic extended with modulo counting quantifiers
• Linear quantifier elimination as an abstract decision procedure
• Certified reasoning with infinity

Describes a project that uses

Uses Software

• REDLOG

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3644100)