In mathematics, BCI and BCK algebras are algebraic structures, introduced by Y. Imai, K. Iséki and S. Tanaka in 1966, that describe fragments of the propositional calculus involving implication known as BCI and BCK logics.
An algebra of type is called a BCI-algebra if, for any , it satisfies the following conditions. (Informally, we may read as "truth" and as " implies ".)