An efficient quantifier elimination procedure for Presburger arithmetic

DOI10.4230/LIPICS.ICALP.2024.142MaRDI QIDQ6875036zbMATH OpenFDO

Authors Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, Georg Zetzsche

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ICALP.2024.142

zbMATH Keywords

convex geometryparametric integer programmingPresburger arithmeticquantifier elimination

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• A Bound on Solutions of Linear Integer Equalities and Inequalities
• Algorithmic analysis of programs with well quasi-ordered domains.
• Approximate formulas for some functions of prime numbers
• Automata Presenting Structures: A Survey of the Finite String Case
• Bounded Regular Sets
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• Dominoes and the complexity of subclasses of logical theories
• scientific article; zbMATH DE number 4030997 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1253963 (Why is no real title available?)
• scientific article; zbMATH DE number 1157651 (Why is no real title available?)
• scientific article; zbMATH DE number 1870066 (Why is no real title available?)
• scientific article; zbMATH DE number 1395614 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• Minimal solutions of linear diophantine systems : bounds and algorithms
• Monadic decomposition
• Monadic decomposition in integer linear arithmetic
• On Chebyshev-Type Inequalities for Primes
• On the existential theories of Büchi arithmetic and linear p-adic fields
• Presburger arithmetic with bounded quantifier alternation
• Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
• Résolution d'une question relative aux déterminants.
• Sensitivity theorems in integer linear programming
• Subclasses of Presburger arithmetic and the weak EXP hierarchy
• The complexity of almost linear diophantine problems
• The complexity of Presburger arithmetic with bounded quantifier alternation depth
• The Well Structured Problem for Presburger Counter Machines
• Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt.
• Well-structured transition systems everywhere!

Cited in

(3)

• Relatively complete and efficient partial quantifier elimination
• An introduction to the theory of linear integer arithmetic (invited paper)
• Title not available (Why is no real title available?)

This page was built for publication: An efficient quantifier elimination procedure for Presburger arithmetic

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