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

arXiv: https://arxiv.org/abs/2205.08297 · HTML: https://mlsanity.com/paper/2205.08297/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 May 2022.

## Built on by (most cited first, 1 of 1)

- [SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning](https://mlsanity.com/paper/2305.12926/) (2023)

## Abstract (arXiv)

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.