一句话：确定子词序上一阶逻辑的可判定边界，并证明所有变量交替受限时整一阶理论可判定。
本文研究有限词上子词序关系的一阶逻辑，其中每个词可作为常量使用。首先证明 Σ1 理论不可判定，即使字母表仅含两个字母。为确定可判定边界，作者考虑交替受限片段：除若干变量外，其余变量只能量词化到字母交替次数有界的语言上。主要结果为：至多两个变量不受交替限制时，Σ1 片段可判定；三个变量不受限时变为不可判定。对于更高的量词交替深度，Σ2 片段在仅一个变量不受交替界限制时已不可判定；而当所有变量都交替受限时，整个一阶理论可判定。
We consider first-order logic over the subword ordering on finite words where each word is available as a constant. Our first result is that the Σ1 theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the Σ1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the Σ2 fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{HalfonSZ17,
title = {Decidability, complexity, and expressiveness of first-order logic over the subword ordering},
author = {Simon Halfon and Philippe Schnoebelen and Georg Zetzsche},
booktitle = {LICS},
year = {2017},
doi = {10.1109/lics.2017.8005141}
}