Skip to main content

First-order Logic Over the Sub-word Ordering

Georg Zetzsche ( LSV Cachan )

This talk reports on results concerning first-order logic over the subword ordering on finite words. It has been known since 2006 that the whole first-order logic over this structure is undecidable, whereas the Sigma_1 fragment is NP-complete. One might therefore expect that introducing each word as a constant would leave the Sigma_1 fragment decidable.  However, it was shown recently that in the presence of these constants, the \Sigma_1 theory becomes undecidable (already over two letters).

Regarding the decidability border, we will consider fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations.  Here, the second result is that when at most two variables are not alternation bounded, the \Sigma_1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded.  Concerning higher quantifier alternation depths, the \Sigma_2 fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable. If time permits, complexity aspects will be treated as well.

This is joint work with Simon Halfon and Philippe Schnoebelen (to be presented at LICS 2017).

Share this: