Kenneth Kunen

Herbert Kenneth Kunen (August 2, 1943August 14, 2020) was an American professor of mathematics at the University of Wisconsin–Madison. 
He worked in set theory. He also worked on non-associative algebraic systems, such as loops, and used computer software, such as the Otter theorem prover, to derive theorems in these areas.