  In \cite{LC, LCMF}, it was introduced a logic (called \Six ) associated to a
class of algebraic structures known as {\em involutive Stone algebras}. This
class of algebras, denoted by \Sto , was considered by the first time in
\cite{CS1} as a tool for the study of certain problems connected to the theory
of finite--valued \L ukasiewicz--Moisil algebras. In fact, \Six\ is the logic
that preserves degrees of truth with respect to the class \Sto .
  Among other things, it was proved that \Six\ is a 6--valued logic that is a
{\em Logic of Formal Inconsistency} (\LFI ); moreover, it is possible to define
a consistency operator in terms of the original set of connectives. A
Gentzen-style system (which does not enjoy the cut--elimination property) for
\Six\ was given. Besides, in \cite{LCMF}, it was shown that \Six\ is matrix
logic that is determined by a finite number of matrices; more precisely, four
matrices. However, this result was further sharpened in \cite{SMUR} proving
that just one of these four matrices determine \Six , that is, \Six\ can be
determined by a single 6--element logic matrix.
  In this work, taking advantage of this last result, we apply a method due to
Avron, Ben-Naim and Konikowska \cite{Avron02} to present different Gentzen
systems for \Six\ enjoying the cut--elimination property. This allows us to
draw some conclusions about the method as well as to propose additional tools
for the streamlining process. Finally, we present a decision procedure for
\Six\ based in one of these systems.
