Download PDFOpen PDF in browserLinear Refutation and Clause SplittingEasyChair Preprint 942310 pages•Date: December 5, 2022AbstractLinear resolution is one of the ancient methods for first-order theorem proving. We extend linear resolution with clause splitting, producing subgoals dispatched independently. An incremental SAT solver keeps track of refutations and thus provides a “lemma” mechanism. We describe some implementation considerations, present some initial experimental results, and discuss future directions for this approach. Keyphrases: Boolean satisfiability, clause splitting, linear resolution
|