# SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 47 references that are in the map.
- First posted on arXiv 22 May 2023.

## Builds on (most cited first, 3 of 3)

- [A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic](https://mlsanity.com/paper/2201.09769/) (2022)
- [SCL(EQ): SCL for First-Order Logic with Equality](https://mlsanity.com/paper/2205.08297/) (2022)
- [SCL(FOL) Revisited](https://mlsanity.com/paper/2302.05954/) (2023)

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

- [Extending SMT Solving with Non-Ground Clause Learning](https://mlsanity.com/paper/2609.11509/) (2026)

## Abstract (arXiv)

We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. The completeness proof of superposition relies on the grounding of the clause set. It builds a ground partial model according to the fixed ordering, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. We define a respective strategy for the SCL calculus such that clauses learned by SCL and superposition inferences coincide. From this perspective the SCL calculus can be viewed as a generalization of the superposition calculus.