2026-10-06T10:54:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25451 2026-03-19T12:28:43Z ddc:004 open_access

Analysis of Logics with Arithmetic Benedikt, Michael Lu, Chia-Hsuan Tan, Tony Presburger quantifiers Spectrum Guarded logics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael Benedikt and Chia-Hsuan Lu and Tony Tan 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.27 urn:nbn:de:0030-drops-254510 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.27 eng https://creativecommons.org/licenses/by/4.0/legalcode