Describing a Basis in Semireduced Form for Inference Rules of Intuitionistic Logic

It is shown that a set of all rules in semireduced form whose premises satisfy a collection of specific conditions form a basis for all rules admissible in IPC. The conditions specified are quite natural, and many of them show up as properties of maximal theories in the canonical Kripke model for IPC. Besides, a similar basis is constructed for rules admissible in the superintuitionistic logic KC, a logic of the weak law of the excluded middle.