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.

In Lewin et al. 359–386) the authors proved that certain systems of annotated logics are algebraizable in the sense of Block and Rigozzi 396). Later in Lewin et al. the study of the associated quasi-varieties of annotated algebras is initiated. In this paper we continue the study of the these classes of algebras, in particular, we report some recent results about the free annotated algebras.

The study of paraconsistent logic as a branch of mathematics and logic has been pioneered by Newton da Costa. With the growing advent of distributed and often inconsistent databases over the last ten years, there has been growing interest in paraconsistency amongst researchers in databases and knowledge bases. In this paper, we provide a brief survey of work in paraconsistent databases and knowledge bases affected by Newton da Costa's important and lasting contributions to the field.