在可判定的一阶逻辑片段中添加圆谬论：复杂度上下起伏
内容提要
本文探讨了描述逻辑及其推理的计算复杂性，包括可判定性和复杂度的多种情况。研究了不同逻辑的组合复杂性，提出了高效的模型采样算法，并探讨了广义一阶决策图的启发式推理算法及其应用。
延伸解读
研究范围与核心问题
本文聚焦于描述逻辑及其推理的计算复杂性，核心问题是在可判定的一阶逻辑片段中，添加圆谬论（circumscription）后，复杂度如何变化。文章涵盖了从ALC到ALCIO和ALCQO等不同描述逻辑，复杂度范围从NExpTime^NP到不可判定，并探讨了组合复杂性和数据复杂性。
关键技术与方法
文章提出了高效的模型采样算法，将双变量逻辑FO^2的采样结果扩展到整个FO^2片段，并支持数量约束。此外，研究了广义一阶决策图（GFODD）的启发式推理算法，在预期模型大小已知时，证明其计算问题可在多项式函数层次内解决。
主要结果与影响
研究证明，在包含任意数量传递关系的一元否定分段中，有限可满足性问题是可判定且2-ExpTime完全的。同时，将对称加权一阶模型计数（WFOMC）的多项式时间可解性扩展到FO^2的特定句子和一维均匀片段，并给出了一阶前缀类的完整分类。
应用与意义
提出的采样算法在组合结构生成、统计关系模型、马尔可夫逻辑网络和概率逻辑程序等领域有潜在应用。此外，关于存在规则与传递性组合的研究为本体规范提供了形式化方法，并给出了查询重写算法，有助于知识库的推理与查询。
Q&A
描述逻辑的计算复杂性有哪些主要范围？
描述逻辑的计算复杂性范围从 NExpTime^NP 到不可判定。
什么是有限可满足性问题，它的复杂性如何？
有限可满足性问题在包含任意数量的传递关系的一元否定分段中是可判定且为 2-ExpTime 完全问题。
高效的模型采样算法有什么应用？
高效的模型采样算法在组合结构、统计关系模型的均匀生成以及 Markov 逻辑网络和概率逻辑程序的采样方面有潜在应用。
广义一阶决策图的启发式推理算法有什么特点？
广义一阶决策图的启发式推理算法在假设预期模型的大小已知时，计算问题可在多项式函数层次内解决。
如何将传递性与可判定类的存在规则结合？
可以通过形式化方法安全添加传递性，并给出相应的查询重写算法。
在一阶逻辑中，FO^2 的采样算法有什么新进展？
FO^2 的采样算法在域大小多项式时间下运行，并能处理复杂的量化器公式。
