One-Variable Logic Meets Presburger Arithmetic

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

One-Variable Logic Meets Presburger Arithmetic

Bartosz BednarczykBartosz Bednarczyk
One-Variable Logic Meets Presburger Arithmetic


Bartosz Bednarczyk
One-Variable Logic Meets Presburger Arithmetic
Theoretical Computer Science, 802(141-146), January 2020
  • 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}
}