A note on monothetic BCI (Q2372686)

The authors prove a conjecture from [\textit{L. Humberstone}, Notre Dame J. Formal Logic 47, No. 1, 101--131 (2006; Zbl 1107.03018)] that the extension of the logic BCI by the axiom \((A \rightarrow A) \rightarrow (B \rightarrow B)\) is monothetic BCI, i.e., the smallest extension of BCI in which all theorems are provably equivalent. The proof is obtained with the help of the automated theorem prover OTTER.