SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
This is an incremental theoretical result for automated theorem proving in logic, showing equivalence between two calculi.
The paper demonstrates that the SCL(FOL) calculus can simulate the derivation of non-reedundant clauses by superposition for first-order logic without equality, showing that clauses learned by SCL and superposition inferences coincide, thus generalizing the superposition calculus.
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.