Automated deduction, or automated theorem proving is a branch of science that deals with automatic search for a proof. The contribution of Kanger to automated deduction is well-recognized. His monograph [1957] introduced a calculus LC, which was one of the first calculi intended for automated proof-search. His article [1963] was later republished as [Kanger 1983] in the collection of “classical papers on computational logic”. [1963] (and also [1959]) calculi used some interesting features that have not been noted for a number of years, and the importance of which in the area of automated deduction has been recognized only much later.