Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership
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$...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5206/pdf |
| _version_ | 1797268566601367552 |
|---|---|
| author | Andreas Krebs Kamal Lodaya Paritosh K. Pandya Howard Straubing |
| author_facet | Andreas Krebs Kamal Lodaya Paritosh K. Pandya Howard Straubing |
| author_sort | Andreas Krebs |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:31Z |
| format | Article |
| id | doaj.art-72ce23cd8d964592a9fddf6c83e43836 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:31Z |
| publishDate | 2020-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-72ce23cd8d964592a9fddf6c83e438362024-03-08T10:31:24ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-09-01Volume 16, Issue 310.23638/LMCS-16(3:16)20205206Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membershipAndreas KrebsKamal LodayaParitosh K. PandyaHoward StraubingWe 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.https://lmcs.episciences.org/5206/pdfcomputer science - logic in computer science |
| spellingShingle | Andreas Krebs Kamal Lodaya Paritosh K. Pandya Howard Straubing Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership Logical Methods in Computer Science computer science - logic in computer science |
| title | Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership |
| title_full | Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership |
| title_fullStr | Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership |
| title_full_unstemmed | Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership |
| title_short | Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership |
| title_sort | two variable logics with some betweenness relations expressiveness satisfiability and membership |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/5206/pdf |
| work_keys_str_mv | AT andreaskrebs twovariablelogicswithsomebetweennessrelationsexpressivenesssatisfiabilityandmembership AT kamallodaya twovariablelogicswithsomebetweennessrelationsexpressivenesssatisfiabilityandmembership AT paritoshkpandya twovariablelogicswithsomebetweennessrelationsexpressivenesssatisfiabilityandmembership AT howardstraubing twovariablelogicswithsomebetweennessrelationsexpressivenesssatisfiabilityandmembership |