Kenneth Kunen
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.