Shortest axiomatizations of implicational S4 and S5 (Q1430904)

The paper introduces several shortest possible axiomatizations for the strict implicational fragments of the modal logics S4 and S5 (which are usually denoted C4 and C5). The paper has three clearly separated parts: the first one deals with the axiomatization of C4. After a brief historical survey of the history of its different axiomatizations, two minimal 2-bases for C4 are given together with a single axiom base, solving an open problem first stated by \textit{A. R. Anderson} and \textit{N. D. Belnap jun.} [Entailment. The logic of relevance and necessity. Vol. I, Princeton, N. J.: Princeton University Press (1975; Zbl 0323.02030)]. Then, a similar section is dedicated to C5, for which a minimal 2-basis is given together with several shortest single axiom bases. All the proofs reported were discovered with the assistance of the automated reasoning program Otter. The final part of the paper outlines the approach used to obtain the results and the automated reasoning strategies used.