论文标题
SCL（EQ）：SCL的一阶逻辑，具有平等
SCL(EQ): SCL for First-Order Logic with Equality
论文作者
论文摘要
我们为一阶逻辑提出了一个新的微积分SCL（EQ），其平等性仅学习非冗余从句。遵循CDCL（冲突驱动子句学习）和SCL（从简单模型学习）的想法，使用地面字面模型假设来指导推断，然后保证这些假设是非冗余的。冗余是根据从地面文字模型假设得出的动态变化排序定义的。我们证明了SCL（EQ）声音并完整，并提供了示例，使我们的演算在叠加方面有所改善。
We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition.
