Analysis of logics with arithmetic
Abstract
We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional ``global cardinality constraints'': restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.
Keywords
Cite
@article{arxiv.2508.03574,
title = {Analysis of logics with arithmetic},
author = {Michael Benedikt and Chia-Hsuan Lu and Tony Tan},
journal= {arXiv preprint arXiv:2508.03574},
year = {2025}
}