×

Short conjunctive normal forms in finitely valued logics. (English) Zbl 0818.03003

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)

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)

Software:

SATCHMO; SETHEO
PDFBibTeX XMLCite
Full Text: DOI