Hähnle, Reiner Short conjunctive normal forms in finitely valued logics. (English) Zbl 0818.03003 J. Log. Comput. 4, No. 6, 905-927 (1994). This paper deals with resolution theorem proving in many-valued logic. The latter has found increasing applications in such diverse fields as nonmonotonic reasoning, error-correcting codes, and software/hardware verification. Here, very long nonclausal formulae naturally come out, and efficient normal form reductions are, if not a sine qua non, at least a very interesting tool for the algorithmic manipulation of these formulas. The author develops a satisfiability preserving CNF reduction of formulas in finite-valued calculi. Generalizing Tseitin’s structure preserving clause forms, and adapting the notion of polarity to the many- valued case, he is able to keep the length of the resulting formulas polynomially bounded with respect to the length of the input formulas, while avoiding the generation of redundant clauses. Formulas are labelled by signs which, in contrast to the two-valued case, are sets of truth values, rather than truth values. The author compares his work with previous results on many-valued normal forms by Baaz, Carnielli, Fernmüller, Morgan, Murray, O’Hearn, Orlowska, Rosenthal, Stachniak, and others. In a final section he discusses applications of his techniques to the many-valued counterparts of the existential and universal quantifiers. Reviewer: D.Mundici (Milano) Cited in 12 Documents MSC: 03B35 Mechanization of proofs and logical operations 03B50 Many-valued logic 03G20 Logical aspects of Łukasiewicz and Post algebras 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:Łukasiewicz logic; resolution theorem proving; many-valued logic; satisfiability preserving CNF reduction of formulas in finite-valued calculi Software:SATCHMO; SETHEO PDFBibTeX XMLCite \textit{R. Hähnle}, J. Log. Comput. 4, No. 6, 905--927 (1994; Zbl 0818.03003) Full Text: DOI