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
Bartosz Bednarczyk
One-Variable Logic Meets Presburger Arithmetic
Theoretical Computer Science, to appear
  • 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.
  • Forschungsgruppe:Research Group: Computational 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}
}