The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Given a set of first-order clauses and a set of ground literals, our lifted two-watched literal scheme efficiently detects all propagating and false clauses with respect to the ground literals. We present the algorithm as a system of rules and prove its soundness and completeness. Additionally, we provide an implementation of the two-watched literal scheme, which outperforms a standard dynamic programming approach for detecting propagatable literals and conflicts, especially when dealing with long clauses.

翻译：双监视文字方案是命题逻辑中高效CDCL（冲突驱动子句学习）实现的核心组成部分，现被扩展至一阶逻辑。给定一组一阶子句和一组基文字，我们的提升式双监视文字方案能够高效检测所有相对于基文字而言的传播子句和假子句。我们将该算法呈现为规则系统，并证明其可靠性与完备性。此外，我们提供了双监视文字方案的实现，该实现优于标准的动态规划方法，特别在处理长子句时，能够更有效地检测可传播文字与冲突。