
I argued in my D.Phil. thesis that when we reason about infinitistic objects in mathematics, we're really reasoning about finite projections of them. I was led to this conclusion by (among other things) the crucial role of pictures in mathematical reasoning.
After working with computers for a few years, I started wondered whether diagrams could help a computer prove theorems automatically. Other researchers were getting interested in diagrammatic reasoning around the same time.
My work  most of it a collaboration with Dave BarkerPlummer  addressed theorem proving in set theory. Some of the results are nondiagrammatic: for example, a lambdaunification algorithm for set theory, and the Zmatch inference rule.
We developed a graphical prover, Grover, which was able to prove some nontrivial theorems with the help of diagrams. The diagrams suggest a series of existence proofs to be carried out as steps toward the main theorem. The "diagrammatic reasoning" consists of figuring out what existence proofs need to be performed, and in what order.