ABSTRACT We show that there is a polynomial over the rational number field corresponding to each propositional formula in a given many-valued logic. To decide whether a propositional formula can be deduced from a finite set of such formulas (deduction problem), we only need to decide whether a polynomial vanishes on an algebraic variety. By using Wu's method, an algorithm for this problem is presented.

ABSTRACT We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete.

The closed world assumption plays a fundamental role in the theory of deductive databases. On the other hand, multi-valued logics occupy a vast field in non-classical logics. Some questions are better explained and expressed in terms of such logics. To enhance the expressive power and the declarative ability of a deductive database, we extend various CWA formalizations, including the naive CWA, the generalized CWA and the careful CWA, to multi-valued logics. The basic idea is to embed logic formulae into some (...) polynomial ring. The extensions can be applied in a uniform manner to any finitely multi-valued logics. Therefore they have also computational interest. (shrink)