ON SKOLEMIZATION AND PROOF COMPLEXITY

Article type: Research Article

Authors: Baaz, Matthias | Leitsch, Alexander

Affiliations: Institut für Algebra und Diskrete Mathematik, Technische Universität Wien, Wiedner Hauptstraβe 8-10, A-1040 Wien, Austria | Institut für Computersprachen, Technische Universität Wien, Resselgasse 3, A-1040 Wien, Austria, email, leitsch@csdecl.twwien.ac.at

Abstract: The impact of Skolemization on the complexity of proofs in the sequent calculus is investigated. It is shown that prefix Skolemization may result in a nonelementary increase of Herbrand complexity (i. e. the minimal number of constituents in a Herbrand disjunction) versus structural Skolemization. Moreover it is shown that restricting the range of quantifiers never increases Herbrand complexity. The results provide a general mathematical justification for minimizing the range of quantifiers (by means of shifting) before Skolemization of formulas.

DOI: 10.3233/FI-1994-2044

Journal: Fundamenta Informaticae, vol. 20, no. 4, pp. 353-379, 1994