One-Variable Logic Meets Presburger Arithmetic

Bartosz BednarczykBartosz Bednarczyk

DOI Link

Bartosz Bednarczyk
One-Variable Logic Meets Presburger Arithmetic
Theoretical Computer Science, to appear

Details
Bibtex

KurzfassungAbstract
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 Image 1-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{B2019,
  author    = {Bartosz Bednarczyk},
  title     = {One-Variable Logic Meets Presburger Arithmetic},
  journal   = {Theoretical Computer Science},
  publisher = {Elsevier},
  year      = {2019},
  month     = {September},
  doi       = {10.1016/j.tcs.2019.09.028}
}