The Gentzenization and decidability of RW (Q911575)

By extending the approach of \textit{J. M. Dunn} presented in the monumental monography ``Entailment. The logic of relevance and necessity. Vol. I'' (1975; Zbl 0323.02030) by \textit{A. R. Anderson} and \textit{N. D. Belnap} jun., the author presents a cut-free Gentzen-type formulation of the relevant system RW. The treatment of negation is similar to that of \textit{R. A. Bull} for the fragment of RW without distribution [Notre Dame J. Formal Logic 28, 220-237 (1987; Zbl 0648.03007)] and that of \textit{I. D. Zaslavskij} for Nelson's logic of constructible falsity [Symmetric constructive logic (in Russian), Armenian Academy of Sciences (Erevan, 1978)]. In order to get decidability for RW, \textit{S. Giambrone}'s decidability argument is used [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)].