Name
Abstract | ||
|---|---|---|
We study an extension 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'. This is, in a sense, the simplest property that is 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 also give an effective necessary condition, in terms of the syntactic monoid of a regular language, for a property to be expressible in this logic. We show that this condition is also sufficient for words over a two-letter alphabet. This algebraic analysis allows us us to prove, among other things, that our new logic has strictly less expressive power than full first-order logic FO[<]. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2933575.2935308 | LICS |
Keywords | Field | DocType |
syntactic monoid,two-letter alphabet,first-order logic FO,variable logic,finite words,two-variable atomic formulas,two-variable logic,algebraic analysis | Discrete mathematics,Combinatorics,Upper and lower bounds,Satisfiability,Algebraic analysis,Syntactic monoid,Regular language,Expressive power,Mathematics,Higher-order logic,Alphabet | Conference |
ISSN | ISBN | Citations |
1043-6871 | 978-1-4503-4391-6 | 2 |
PageRank | References | Authors |
0.40 | 17 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Krebs | 1 | 21 | 8.20 |
| Kamal Lodaya | 2 | 225 | 19.53 |
| Paritosh K. Pandya | 3 | 944 | 91.64 |
| Howard Straubing | 4 | 528 | 60.92 |