RESOLUTION AND PATH DISSOLUTION IN MULTIPLE-VALUED LOGICS

Path dissolution is an inferencing mechanism for classical logic that efficiently generalizes the method of analytic tableaux. Two features that both methods enjoy are (in the propositional case) strong completeness and the ability to produce a list of essential models (satisfying interpretations) of a formula. The latter feature is particularly valuable in a setting in which one wishes to make use of satisfying interpretations rather than merely to determine whether any exist In this paper we describe a method for employing dissolution as a deduction mechanism for a class of multiple-valued logics that we call the UNF logics. The basic idea is to keep track of the sign of the formula. Dissolution is shown to be a sound rule of inference as well as strongly complete in this setting. We also describe how the signing technique may be used to apply resolution to these logics; Robinson's semantic tree argument is adapted to prove completeness.