One-Variable Logic Meets Presburger Arithmetic
Logic in Computer Science
2019-09-17 v3
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.
Keywords
Cite
@article{arxiv.1810.10899,
title = {One-Variable Logic Meets Presburger Arithmetic},
author = {Bartosz Bednarczyk},
journal= {arXiv preprint arXiv:1810.10899},
year = {2019}
}
Comments
A short note accepted to TCS