Etessami et al. [5] showed that satisfiability of two-variable first order logic (Formula presented) on word models is Nexptime-complete. We extend this upper bound to the slightly stronger logic (Formula presented), which allows checking whether a word position is congruent to r modulo q, for some divisor q and remainder r. If we allow the more powerful modulo counting quantifiers of Straubing, Thérien et al. [22] (we call this two-variable fragment (Formula presented) satisfiability becomes Expspace-complete. A more general counting quantifier, (Formula presented) makes the logic undecidable.
CITATION STYLE
Lodaya, K., & Sreejith, A. V. (2017). Two-variable first order logic with counting quantifiers: Complexity results. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10396 LNCS, 260–271. https://doi.org/10.1007/978-3-319-62809-7_19
Mendeley helps you to discover research relevant for your work.