Analysis of logics with arithmetic

TL;DR

This paper investigates the finite satisfiability problem for logics combining counting and arithmetic, providing complexity bounds, semilinear representations, and simplified proofs for key results in the field.

Contribution

It offers a tight complexity bound for local Presburger quantifiers and introduces a method to compute semilinear representations for two-variable logic with counting, enhancing understanding of satisfiability with global constraints.

Findings

Tight bound on satisfiability complexity for local Presburger quantifiers

Semilinear representation of cardinalities in two-variable logic with counting

Simplified proofs of key results on finite satisfiability and spectrum semi-linearity

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.