SAT-Based Subsumption Resolution

Coutelier, R; Kovács, L; Rawson, M; Rath, J

Coutelier, R (通讯作者),Univ Liege, Liege, Belgium.

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

Abstract

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-bas......

Full Text Link