On the value of antiprenexing

Autor: Uwe Egly
Rok vydání: 1994
Předmět:
Zdroj: Logic Programming and Automated Reasoning ISBN: 9783540582168
LPAR
DOI: 10.1007/3-540-58216-9_30
Popis: 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.
Databáze: OpenAIRE