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

From MaRDI portal
scientific article
Language Label Description Also known as
English
On different structure-preserving translations to normal form
scientific article

    Statements

    On different structure-preserving translations to normal form (English)
    0 references
    0 references
    6 March 1997
    0 references
    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.
    0 references
    automated deduction
    0 references
    structure-preserving normal forms
    0 references
    Herbrand complexity
    0 references

    Identifiers