@online{Leidinger2205.08297,
TITLE = {{SCL}({EQ}): {SCL} for First-Order Logic with Equality},
AUTHOR = {Leidinger, Hendrik and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2205.08297},
EPRINT = {2205.08297},
EPRINTTYPE = {arXiv},
YEAR = {2022},
ABSTRACT = {We propose a new calculus SCL(EQ) for first-order logic with equality that<br>only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven<br>Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal<br>model assumption is used to guide inferences that are then guaranteed to be<br>non-redundant. Redundancy is defined with respect to a dynamically changing<br>ordering derived from the ground literal model assumption. We prove SCL(EQ)<br>sound and complete and provide examples where our calculus improves on<br>superposition.<br>},
}