两变量逻辑与某些中间关系：表达能力、可满足性和成员资格
摘要：使用有限字串中解释的一阶逻辑 FO2[<]，我们研究了两个扩展，在这些扩展中，公式只能使用两个变量。我们在这个语言中添加了两个变量的原子公式，分别表示“字母 $a$ 出现在位置 $x$ 和 $y$ 之间”和“因子 $u$ 出现在位置 $x$ 和 $y$ 之间”。从某种意义上说，这些是最简单的不能仅使用两个变量表达的属性。 我们提出了多个逻辑，包括一阶逻辑和时态逻辑，它们具有相同的表达能力，并为每个公式的可满足性的复杂性找到了相匹配的下界和上界。我们给出了一些有效的条件，以正则语言的语法单子群的形式，用来判断一个属性是否可以在这些逻辑中表达。这种代数分析使我们能够证明，我们的新逻辑比全面的一阶逻辑 FO[<]具有更少的表达能力。我们的证明需要开发出与字串因子分解相关的新技术。
作者：Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, Howard Straubing
论文ID：1902.05905
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22