Quantifier elimination for counting extensions of Presburger arithmetic

Quantifier elimination for counting extensions of Presburger arithmetic

We give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier ∃=xyΦ that binds to the variable x the number of different y satisfying Φ. While our procedure runs in non-elementary time in general, we show that it yields nearly optimal elementary c...

Descripció completa

Dades bibliogràfiques
Autors principals:	Chistikov, D, Haase, C, Mansutti, A
Format:	Conference item
Idioma:	English
Publicat:	Springer 2022

Ítems similars

The complexity of Presburger arithmetic with power or powers
per: Benedikt, M, et al.
Publicat: (2023)

On Presburger arithmetic extended with non-unary counting quantifiers
per: Peter Habermehl, et al.
Publicat: (2023-07-01)

Beyond quantifier-free interpolation in extensions of presburger arithmetic
per: Brillout, A, et al.
Publicat: (2011)

An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
per: Brillout, A, et al.
Publicat: (2011)

An interpolating sequent calculus for quantifier-free Presburger arithmetic
per: Brillout, A, et al.
Publicat: (2011)

Quantifier-Free Boolean Algebra with Presburger Arithmetic is NP-Complete
per: Kuncak, Viktor
Publicat: (2007)

Extensions of Presburger arithmetic and model checking one-counter automata
per: Lechner, A
Publicat: (2016)

Geometric decision procedures and the VC dimension of linear arithmetic theories
per: Chistikov, D, et al.
Publicat: (2022)

On the decidability of Presburger arithmetic expanded with powers
per: Karimov, T, et al.
Publicat: (2025)

Presburger Arithmetic with algebraic scalar multiplications
per: Philipp Hieronymi, et al.
Publicat: (2021-07-01)

Super-exponential Complexity of Presburger Arithmetic
per: Fischer, Michael J., et al.
Publicat: (2023)

Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
per: Haase, C, et al.
Publicat: (2019)

Abstraction−based Satisfiability Solving of Presburger Arithmetic
per: Kroening, D, et al.
Publicat: (2004)

Unification modulo presburger arithmetic and other decidable theories
per: Mauricio Ayala Rincón, et al.
Publicat: (2001-12-01)

An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
per: Kuncak, Viktor, et al.
Publicat: (2005)

Parametric Presburger arithmetic: logic, combinatorics, and quasi-polynomial behavior
per: Tristram Bogart, et al.
Publicat: (2017-01-01)

Higher-order quantified boolean satisfiability
per: Chistikov, D, et al.
Publicat: (2022)

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
per: Anthony W. Lin, et al.
Publicat: (2021-10-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
per: Sanjit A. Seshia, et al.
Publicat: (2005-12-01)

On deciding linear arithmetic constraints over -adic integers for all primes
per: Haase, C, et al.
Publicat: (2021)

On the complexity of quantified integer programming
per: Chistikov, D, et al.
Publicat: (2017)

Enrichments of Boolean algebras by Presburger predicates
per: Derakhshan, J, et al.
Publicat: (2017)

Model theory of finite-by-Presburger Abelian groups and finite extensions of $p$-adic fields
per: Derakhshan, J, et al.
Publicat: (2016)

Deciding whether the ordering is necessary in a Presburger formula
per: Christian Choffrut, et al.
Publicat: (2010-01-01)

Counting and Arithmetic of the Inca
per: Ximena Catepillán, et al.
Publicat: (2012-01-01)

On two-variable guarded fragment logic with expressive local Presburger constraints
per: Chia-Hsuan Lu, et al.
Publicat: (2024-08-01)

The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
per: leroux jerome
Publicat: (2010-09-01)

On the expressiveness of Büchi arithmetic
per: Haase, C, et al.
Publicat: (2021)

Counting and configurations : problems in combinatorics, arithmetic, and geometry /
per: 243906 Herman, Jiri, et al.
Publicat: (2003)

Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic
per: Federico Aschieri, et al.
Publicat: (2012-10-01)

About the possibility of the extension of the additive arithmetic
per: Livija Maliaukienė
Publicat: (2002-12-01)

ISA Extensions for Finite Field Arithmetic
per: Erdem Alkim, et al.
Publicat: (2020-06-01)

The cognitive foundations of early arithmetic skills: It is counting and number judgment, but not finger gnosis, that count
per: Long, I, et al.
Publicat: (2017)

The taming of the semi-linear set
per: Chistikov, D, et al.
Publicat: (2016)

An arithmetic regularity lemma, associated counting lemma, and applications
per: Green, B, et al.
Publicat: (2010)

Approximate counting in SMT and value estimation for probabilistic programs
per: Chistikov, D, et al.
Publicat: (2017)

Modal logics and local quantifiers: A zoo in the elementary hierarchy
per: Fervari, R, et al.
Publicat: (2022)

A complete axiomisation for quantifier-free separation logic
per: Demri, S, et al.
Publicat: (2021)

Context-free commutative grammars with integer counters and resets
per: Chistikov, D, et al.
Publicat: (2016)

The effects of adding reachability predicates in quantifier-free separation logic
per: Demri, S, et al.
Publicat: (2021)