About
Michael thinks that computers ought to be able to reason and learn from their past experiences. He is particularly interested in automated theorem proving: computer systems that make watertight logical arguments. He is part of a team developing the leading theorem prover Vampire.