On different structure-preserving translations to normal form

DOI10.1006/JSCO.1996.0044MaRDI QIDQ674761zbMATH OpenOpenAlexFDO

Authors Uwe Egly

Publication date 6 March 1997

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.1996.0044

zbMATH Keywords

automated deductionHerbrand complexitystructure-preserving normal forms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Review text

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.

Recommendations

• On the practical value of different definitional translations to normal form
• Practically useful variants of definitional translations to normal form
• A structure-preserving clause form translation
• scientific article; zbMATH DE number 994053

Cited in

(9)

• A solver for QBFs in negation normal form
• An answer to an open problem of Urquhart
• Practically useful variants of definitional translations to normal form
• scientific article; zbMATH DE number 994053 (Why is no real title available?)
• scientific article; zbMATH DE number 67125 (Why is no real title available?)
• Non-elementary speed-ups in proof length by different variants of classical analytic calculi
• On the practical value of different definitional translations to normal form
• Some pitfalls of \textsf{LK}-to-\textsf{LJ} translations and how to avoid them
• Normalization Issues in Mathematical Representations

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: On different structure-preserving translations to normal form

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q674761)