Unifying Splitting

Ebner, G; Blanchette, J; Tourret, S

Ebner, G (通讯作者),Vrije Univ Amsterdam, Amsterdam, Netherlands.

JOURNAL OF AUTOMATED REASONING, 2023; 67 (2):

Abstract

AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it ......

Full Text Link