Analysis of logics with arithmetic
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917049854328832 |
|---|---|
| author | Benedikt, Michael Lu, Chia-Hsuan Tan, Tony |
| author_facet | Benedikt, Michael Lu, Chia-Hsuan Tan, Tony |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_03574 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Analysis of logics with arithmetic Benedikt, Michael Lu, Chia-Hsuan Tan, Tony Logic in Computer Science 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. |
| title | Analysis of logics with arithmetic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.03574 |