Cut-free sequent-style systems for a logic associated to involutive Stone algebras.

This article focuses on the development of cut-free sequent calculi for the six-valued logic Six, which is associated with the class of involutive Stone algebras. Six is a Logic of Formal Inconsistency (LFI) that preserves degrees of truth relative to these algebras and can be characterized by a single six-element logical matrix. Building on prior results, the authors apply a method by Avron, Ben-Naim, and Konikowska to construct multiple Gentzen-style systems for Six that enjoy the cut-elimination property, culminating in a streamlined system named GSix with 26 logical rules. They further provide a decision procedure based on GSix, enabling bottom-up proof search, and discuss principles and tools to optimize the complexity of the proof systems. The work contributes to the proof-theoretic understanding of Six and suggests directions for extending these methods to other many-valued logics without matrix semantics.