 Skolem was strongly influenced by Schröder’s Algebra der Logik, starting with his PhD Thesis. Later he took a particular interest in the quest for an Elimination Theorem in the calculus of classes. In his 1919 paper he established some results for lattices, in particular, he showed that one could decide the validity of universal Horn sentences (i.e., universal sentences with a matrix that is a disjunction of negated and unnegated atoms, with at most one positive atom) by a procedure that we now recognize to be a polynomial time algorithm. This algorithm was based on finding a least fixed point of a finite partial lattice under production rules derived from universal Horn sentences. Although this result, which is equivalent to the uniform word problem for lattices, was in the same paper as Skolem’s famous contribution to Löwenheim’s Theorem, it was forgotten until a chance rediscovery in the early 1990s. (Whitman (1941) gave a different solution to the more limited equational decision problem for lattices; it became widely known as the solution to the word problem in lattices.)