ADAPTING CLASSICAL INFERENCE TECHNIQUES TO MULTIPLE-VALUED LOGICS USING SIGNED FORMULAS

Abstract

We consider means for adapting classical deduction techniques to multiple-valued logics. Some recent work in this area, including our own, utilizes signs (subsets of the set of truth values). In this paper we develop a language of signed formulas that may be interpreted as a meta-level logic. Questions not expressible in the underlying logic are easily expressed in this meta-logic, and they may be answered with classical techniques because the logic is classical in nature. We illustrate the applicability of classical techniques by adapting resolution, path resolution, and path dissolution to signed formulas. The meta-logic admits a version of Herbrand's Theorem, so that these results extend naturally to the first order case. The fact that annotated logics are a special case of signed formulas is briefly illustrated.