On the value of antiprenexing

In this paper, we examine the effect of antiprenexing on the proof length if resolution deduction concepts are applied. Roughly speaking, our version of antiprenexing moves ∀-quantifiers downward in the formula tree whereas ∃-quantifiers are moved upward. We show that two different Skolemization techniques result in two clause sets with rather different resolution refutations. The lower bounds on the length of both refutations differ exponentially. Furthermore, we demonstrate that both techniques can be improved if antiprenexing is applied before Skolemization. Finally, we examine the influence of antiprenexing if extended resolution deduction concepts are used.