Bounding quantification in parametric expansions of Presburger arithmetic

DOI10.1007/S00153-017-0593-0zbMATH Open1496.03141arXiv1604.06166OpenAlexW2963029392MaRDI QIDQ1661676FDOQ1661676

John Goodrick

Publication date: 16 August 2018

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Abstract: We generalize Cooper's method of quantifier elimination for classical Presburger arithmetic to give a new proof that all parametric Presburger families (as defined by Kevin Woods) are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f over the integers. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic with multiplication by scalars from any ring of functions into Z.

Full work available at URL: https://arxiv.org/abs/1604.06166

Recommendations

• Presburger arithmetic with bounded quantifier alternation
• Parametric Presburger arithmetic: complexity of counting and quantifier elimination
• Complexity of Presburger arithmetic with fixed quantifier dimension
• Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• Publication:4508549
• scientific article; zbMATH DE number 4031630
• On Presburger arithmetic extended with non-unary counting quantifiers
• On Presburger arithmetic extended with modulo counting quantifiers
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic

zbMATH Keywords

Presburger arithmeticelimination of imaginariesbounded quantifiers

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Quantifier elimination, model completeness, and related topics (03C10)

Cites Work

• Title not available (Why is that?)
• Weak quantifier elimination for the full linear theory of the integers
• The parametric Frobenius problem
• The unreasonable ubiquitousness of quasi-polynomials
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (2)

• Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
• Expansions of Presburger arithmetic with the exchange property

This page was built for publication: Bounding quantification in parametric expansions of Presburger arithmetic

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