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

Bromberger, M; Jain, C; Weidenbach, C

Weidenbach, C (通讯作者),Max Planck Inst Informat, Saarbrucken, Germany.

AUTOMATED DEDUCTION, CADE 29, 2023; 14132 (): 134

Abstract

We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-base......

Full Text Link