Part 2. Special Issues in Intellectual Systems Theory

Graph based extended resolution for Boolean formulas

G. V. Bokov


Abstract: In this article we consider a graph based extended resolution for representing refutations of Boolean formulas in conjunction normal form. We prove that a Boolean formula is unsatisfiable iff there is its graph based refutation.

Keywords: Resolution, graph based refutation, unsatisfiability, Boolean formulas.