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
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