.png){kind=icon}
返回
On two-variable first-order logic with a partial order
.png){kind=icon}
PRE
AI
DOI：10.1093/logcom/exaf068.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
本工作的主要动机是关于一阶逻辑的两变量片段FO2（带一个传递关系）的可满足性问题的可判定性这一开放性问题。在存在等式的情况下，该问题可归约为当传递关系被要求为严格偏序时的对应问题。已知其有限可满足性问题可判定，但一般可满足性问题的可判定性仅对受限变体得到解决。更准确地说，该问题在具有可比见证的片段中是可判定的，其中存在量词被要求由形如x < y的原子保护，这一性质与模态逻辑到一阶逻辑的标准翻译一致。我们研究了两种“互补”片段：（i）具有不可比见证的片段，其中公式在否定范式中包含仅应用于形如x similar to y boolean AND ψ的存在量词，其中x similar to y boolean AND表示x和y在序上不可比；（ii）允许可比和不可比见证的片段，但对全称部分施加某些限制。我们证明带偏序和不可比见证的FO2不是局部有限的。在积极方面，我们证明该逻辑具有有限反链性质，我们相信这是证明其可满足性问题的可判定性的关键步骤。我们还确定了保留有限模型属性所需的、对全称部分的最小句法限制。这些限制禁止形如“对所有x, y（Ax boolean AND By -> x sic similar to y）”的语句，其中A和B不同。此外，我们证明在这些限制下，允许可比和不可比见证的片段的可满足性问题可判定。
Keyword:
Two-variable first-order logic
satisfiability problem
decidability
finite model property
transitivity
partial order
finite antichains
locally finite order