One-Variable Logic Meets Presburger Arithmetic

Bartosz BednarczykBartosz Bednarczyk

ISSN: 0304-3975
Download
DOI Link

Bartosz Bednarczyk
One-Variable Logic Meets Presburger Arithmetic
Theoretical Computer Science, 802(141-146), January 2020

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 NP-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{B2020,
  author    = {Bartosz Bednarczyk},
  title     = {One-Variable Logic Meets Presburger Arithmetic},
  journal   = {Theoretical Computer Science},
  volume    = {802},
  number    = {141-146},
  publisher = {Elsevier},
  year      = {2020},
  month     = {January},
  doi       = {10.1016/j.tcs.2019.09.028}
}