Analysis of logics with arithmetic

2025/08/05 by Benedikt, Michael, Lu, Chia-Hsuan, Tan, Tony
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2508.03574

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.

Citations

• On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics
• Two variable logic with ultimately periodic counting
• Regular graphs and the spectra of two-variable logic with counting
• Complexity Results and Practical Algorithms for Logics in Knowledge Representation

Related

• Two variable logic with ultimately periodic counting
• Arithmetic, First-Order Logic, and Counting Quantifiers
• One-Variable Logic Meets Presburger Arithmetic
• Interleaving Logic and Counting
• Counting Computations with Formulae: Logical Characterisations of Counting Complexity Classes