Decidability in the Logic of Subsequences and Supersequences

2015/01/01 by Prateek Karandikar, Philippe Schnoebelen
Computer Science · Mathematics · #AKA #Artificial intelligence #Bounded function #Combinatorics #Computer science #Decidability #Discrete mathematics #Embedding #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Order (exchange) #Sequence (biology) #Subsequence #Undecidable problem #cs.FL #cs.LO #semigroups and automata theory

paper · pdf · doi:10.4230/lipics.fsttcs.2015.84

published as 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

openalex publication_date 2015/01/01 · arxiv created 2015/10/14 · arxiv updated 2016/07/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05

Abstract

We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Sigma₂ theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO² theory is decidable while the FO³ theory is undecidable.

Citations

• The Power of Priority Channel Systems