E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Datum (veröffentlicht):
5-Dez-2022
-
Umfang:
10
-
Preprint-Server:
EasyChair Preprints
-
Keywords:
Boolean satisfiability; clause splitting; linear resolution
en
Abstract:
Linear 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.