Normal form transformations (Q2751356)

This is a detailed overview about normal forms in logic and their transformations. There are various applications of normal forms, like in automated deduction, the reduction of the original inference problem to simple calculi like resolution and paramodulation, and, in general, for the appropriate application of heuristics.NEWLINENEWLINENEWLINEFor example, when working in clausal forms, the whole logical structure of the original formulae is stored in atom formulae, and terms, quantifiers and the logical operators are essentially removed. Many normal form transformations are equivalence-preserving, others, like Skolem normal form, extend the signature of the formula and are not equivalence-preserving. Rather, Skolem normal form preserves satisfiability or validity-equivalence, in the respective application. Also, normal forms in nonclassical logics are considered.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].