A tableau style proof system for two paraconsistent logics (Q1309339)

The paper provides a tableau proof-theory for the propositional logics LP [see the reviewer, J. Philos. Logic 8, 219-241 (1979; Zbl 0402.03012)] and First Degree Entailment [see section 50.3 of \textit{A. R. Anderson}, \textit{N. D. Belnap} and \textit{J. M. Dunn}: Entailment: the logic of relevance and necessity, Vol. II, Princeton University Press (1992)]. The major difference from tableaux for classical logic is that formulas are signed, and the tableaux rules operate on the signs as well as the formulas. Soundness and completeness are established by extensions of the usual classical techniques.