Tree-like proof systems for finitely-many valued non-deterministic consequence relations (Q2228348)

An abstract framework for sequent-based proof systems for non-deterministic logics were constructed in [\textit{A. Avron} and \textit{L. Lev}, J. Log. Comput. 15, No. 3, 241--261 (2005; Zbl 1070.03010)]. The current paper presents an abstract framework for constructing tree-like (tableaux) proof systems for finitely-many valued deterministic and non-deterministic consequence relations. This framework is quite general and there is a mechanical procedure for finding a counter-model for any invalid inference which is an advantage over sequent-based systems. The framework is illustrated for the paraconsistent weak Kleene logic PKW [\textit{S. Bonzio} et al., Stud. Log. 105, No. 2, 253--297 (2017; Zbl 1417.03191)] as a deterministic example and for the non-deterministic examples CLuN [\textit{D. Batens} and \textit{K. De Clercq}, Log. Anal., Nouv. Sér. 47, No. 185--188, 227--257 (2004; Zbl 1078.03024)] and BAT [the author, Log. J. IGPL 26, No. 1, 96--108 (2018; Zbl 1499.03058); the author and \textit{R. Urbaniak}, Rev. Symb. Log. 11, No. 2, 207--223 (2018; Zbl 1502.03005)]. It is shown that the proof systems generated by the framework are complete.