One-Variable Logic Meets Presburger Arithmetic

2018/10/25 by Bednarczyk, Bartosz
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1810.10899

Abstract

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove NP-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.

Related

• Analysis of logics with arithmetic
• Two variable logic with ultimately periodic counting
• Decidable fragments of first-order modal logics with counting quantifiers over varying domains
• Arithmetic, First-Order Logic, and Counting Quantifiers
• One-dimensional fragment of first-order logic