发表机构
University of Wrocław（弗罗茨瓦夫大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文简化了Maslov类K的NExpTime完全性和有限模型性质的证明，并引入扩展类K+E，证明其具有有限模型性质且可满足性问题是2-NExpTime完全的。
AI 中文摘要
Maslov类K是免等式一阶逻辑的一个可判定片段。它包含了许多经典的可判定片段，包括免等式一元片段、免等式二元片段以及Gödel类。该类于50多年前被引入，已在自动推理中主要通过基于归结的方法得到研究。尽管历史悠久，K的可满足性问题的精确复杂度直到最近才被确定，即NExpTime完全性。本工作的两个主要贡献如下：1. 近期关于K的NExpTime完全性和有限模型性质的证明高度非平凡且技术上复杂。我们给出了这两个结果的相当简化的证明。我们的方法将K到可解Skolem句子类的新颖归约与有限模型的随机构造相结合。2. 我们引入了类K+E，允许K中的句子包含一个特殊的二元谓词E，其解释被约束为等价关系。通过将我们的方法应用于这个扩展类，我们证明了K+E具有有限模型性质，并且其可满足性问题是2-NExpTime完全的。
英文摘要
Maslov's class K is a decidable fragment of equality-free first-order logic. It subsumes numerous classical decidable fragments, including the equality-free monadic fragment, the equality-free two-variable fragment, and the Gödel class. Introduced over 50 years ago, the class K has been studied in automated deduction, primarily through resolution-based methods. Despite this long history, the precise complexity of the satisfiability problem for K remained open until recently, when NExpTime-completeness was finally established. The two main contributions of this work are as follows. 1. The recent proofs of NExpTime-completeness and the finite model property for K are highly non-trivial and technically sophisticated. We present considerably simpler proofs of both results. Our approach combines a novel reduction from K to the class of solvable Skolem sentences with a randomised construction of finite models. 2. We introduce the class K+E by allowing sentences in K to contain one distinguished binary predicate E whose interpretation is constrained to be an equivalence relation. By leveraging our approach to this extended class, we prove that K+E has the finite model property and that its satisfiability problem is 2-NExpTime-complete.
CommentsExtended version of an LPAR2026 paper
