Automated deduction for many-valued logics (Q2751372)

This Handbook chapter a reader may use as a comprehensive guide to the contemporary many-valued automated reasoning techniques based on the method of signed formulas. The authors have proved themselves to be good specialists in this field. They give an exposition of the resolution method for first-order finite-valued logics. They consider proof systems with signed formulas, i.e., expressions of many-valued logics that have sets of truth values attached to their heads. Such formulas have two-valued interpretation. The authors describe two kinds of transformations that should be applied to many-valued formulas in order to use them in resolution procedures. These two transformations are language-preserving (CNF) and structure-preserving transformations. Also the resolution inference system is constructed, and refutational and implicational completeness are proved for this system. Transformation and resolution rules are tested with a cute 2-world Kripke model example. There are some hints how one can generalize results concerning the 2-world model to the case of the \(n\)-world model which corresponds to \(2^n\)-valued logic.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].