On different structure-preserving translations to normal form (Q674761)

Most automated deduction methods require to transform logical formulae into a normal form, e.g., clausal form. Clausal form has two well-known weaknesses. First, the application of the distributivity laws during the transformation may increase exponentially the number of literals. Second, the original structure of the problem is lost. For these reasons, various structure-preserving normal forms have been proposed. This paper compares two of them: a definitional normal form and its optimization, called \(p\)-definitional normal form, which generally produces shorter normal forms. The comparison is developed in the context of Gentzen-style calculi, using as measure the Herbrand complexity, or, informally, the size of a shortest proof. It is shown that there exists a sequence of sequents for which the Herbrand complexity grows exponentially, if the definitional form is used, and it grows according to a non-elementary function, if the \(p\)-definitional form is used. Since the non-elementary function grows much faster than an exponential function, this shows that there is a worst-case scenario where the shorter normal form corresponds to a much longer proof.