一句话：研究在有限词上加入 a 或因子 u 介于两位置之间的二变量逻辑，刻画表达力、可满足性复杂度与代数成员判定。
论文研究 FO2[<]（有限词上仅用两个变量的一阶逻辑）的两类扩展：加入二变量原子公式，表示“字母 a 位于位置 x 与 y 之间”以及“因子 u 位于 x 与 y 之间”。这些性质无法仅用两个变量表达。作者给出若干表达力相同的逻辑形式（含一阶与时序逻辑），并为各形式确定可满足性复杂度的上下界。进一步，用正则语言的 syntactic monoid 给出有效条件，判定性质能否在这些逻辑中表达。该代数分析证明新逻辑严格弱于完整 FO[<]；证明依赖关于词因式分解的新技术。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KrebsLPS20,
title = {Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership},
author = {Andreas Krebs and Kamal Lodaya and Paritosh K. Pandya and Howard Straubing},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:16)2020}
}