SCL(EQ): SCL for First-Order Logic with Equality

Hendrik Leidinger, Christoph Weidenbach

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 (…