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

Martin Bromberger, Chaahat Jain, Christoph Weidenbach

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…