Axiomatizing the Skew Boolean Propositional Calculus

The skew Boolean propositional calculus () is a generalization of the classical propositional calculus that arises naturally in the study of certain well-known deductive systems. In this article, we consider a candidate presentation of and prove it constitutes a Hilbert-style axiomatization. The problem reduces to establishing that the logic presented by the candidate axiomatization is algebraizable in the sense of Blok and Pigozzi. In turn, this process is equivalent to verifying four particular formulas are derivable from the candidate presentation. Automated deduction methods played a central role in proving these four theorems. In particular, our approach relied heavily on the method of proof sketches.