NRCL -Bernays-Schönfinkel片段的模型构建方法（全文）
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment (Full Paper)
摘要：
我们结合约束字面量模型表示的关键概念，从一阶叠加和命题冲突驱动的子句学习（CDCL）创建新的演算非冗余子句学习（NRCL）决定Bernays-Schönfinkel片段。我们的演算使用一阶文字约束的元组之间的条件紧凑的模型表示。NRCL继承了叠加的抽象冗余准则和单调模型算子。CDCL增加了对诱导模型的原子排序的动态的、冲突驱动的搜索。因此，在NRCL中，可以有效地以当前模型候选为模来找到假子句。它指导推导一阶有序的预解式，从来没有多余的。类似于CDCL中的1UIP学习，学习的解决方案会导致回溯，并且通过传播阻止先前的冲突状态，它会强制寻找模型或反驳。非冗余的结果也意味着只有1000个子句可以由NRCL在Bernays-Schönfinkel片段上生成，这可以作为终止的论据。
英文摘要：
We combine constrained literals for model representation with key concepts from first-order superposition and propositional conflict-driven clause learning (CDCL) to create the new calculus Non-Redundant Clause Learning (NRCL) deciding the Bernays-Schönfinkel fragment. Our calculus uses first-order literals constrained by disequations between tuples of terms for compact model representation. From superposition, NRCL inherits the abstract redundancy criterion and the monotone model operator. CDCL adds the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be found effectively modulo the current model candidate. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and, by blocking the previous conflict state via propagation, it enforces progress towards finding a model or a refutation. The non-redundancy result also implies that only finitely many clauses can be generated by NRCL on the Bernays-Schönfinkel fragment, which serves as an argument for termination.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
