Extension Rule for Non-Clausal Propositional Calculus

Van Gelder has described a few reasons for satisfiability testing without transformation of formulas into CNF and has developed an algorithm for this problem. We have introduced two possible improvements. First, we have used directed acyclic graphs for the representation of formula, instead of representation in the form of a tree or a string of characters. Second, we have allowed a limited introduction of new variables, again without transformation to CNF. In terms of a proof system, Van Gelder’s algorithm does not p-simulate system described here. Some generalizations of notions of propositional formula, satisfiability, etc. are introduced.