Tableau Systems for Some Paraconsistent Modal Logics

In this paper we present tableau-style proof theories for some modal extensions of two paraconsistent propositional logics: RM3, which allows for truth value gluts, and the weaker BN4, which also allows for truth value gaps. These proof theories are shown to be sound and complete with respect to their corresponding semantics. For comparison, we then present some Hilbert-style axiomatizations of these systems proposed by Lou Goble, and bring out some of the comparative advantages and disadvantages of these vis-à-vis our tableau systems.