Andreas Krebs ; Kamal Lodaya ; Paritosh K. Pandya ; Howard Straubing - Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership

lmcs:5206 - Logical Methods in Computer Science, September 8, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:16)2020
Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membershipArticle

Authors: Andreas Krebs ; Kamal Lodaya ; Paritosh K. Pandya ; Howard Straubing

    We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using only two variables. We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We give effective conditions, in terms of the syntactic monoid of a regular language, for a property to be expressible in these logics. This algebraic analysis allows us to prove, among other things, that our new logics have strictly less expressive power than full first-order logic FO[<]. Our proofs required the development of novel techniques concerning factorizations of words.


    Volume: Volume 16, Issue 3
    Published on: September 8, 2020
    Accepted on: June 8, 2020
    Submitted on: February 23, 2019
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1578 times.
    This article's PDF has been downloaded 299 times.