Abstract:Annotated logic is one of the paraconsistent logics.The entailments in annotated logic are and |≈. Both of them are paraconsistent, and can treat any set of formulae, either consistent or not, in a uniform way. is monotonic, it has a resolution based sound and complete proof procedure, but some rational inferences of the classical logic, such as modus ponens, are no longer valid under it.|≈ is nonmonotonic. The classical inferences hold true under it when there is no contradiction. But no satisfactory proof theory for |≈ has been given. This paper will propose sound and complete decision Tableaux for and |≈ respectively.