 The family of mappings \(\{f_i\}_{i\in I}\) can be shown to define a PTS which characterizes bC in a decidable way (see Carnielli et al. 2008). As an example, it can be easily checked that \(\varphi\wedge\neg\varphi\to\neg{\circ}\varphi\) is a theorem of bC: just consider all its finitely many translations and test that all of them are three-valued tautologies. On the other hand, \(\neg(\varphi\wedge\neg\varphi)\to{\circ}\varphi\) is not a theorem of bC, which can be promptly verified by showing that at least one of its translations is not a tautology using the three-valued tables above. For an alternative PTS characterization of bC and related logics see Marcos 2008.