Sidney Bailin

Computer Scientist

 Automated Theorem Proving

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 Barker-Plummer - addressed theorem proving in set theory. Some of the results are non-diagrammatic: for example, a lambda-unification algorithm for set theory, and the Z-match inference rule.

We developed a graphical prover, Grover, which was able to prove some non-trivial 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.


| Site Map | Contact Me | ©2015 Sidney C. Bailin Valid XHTML 1.0 Strict Valid CSS!