Valuation graphs for propositional logic

In this paper we present the proof system, called the valuation graphs system, which is a new version of two proof procedures: Davis-Putnam and Stålmarck. The novelty is that in the rules we note which propositional variable occurring in some propositional formula does not determine the logical value of that formula. Due to Stålmarck, we define a notion of proof width, corresponding to the width of structure of valuation graph which is a number of applications of dilemma rule. The dilemma rule considers two cases, so the time of proof grows up exponentially.