Dr Mateja Jamnik

Humans often use diagrams for reasoning, but can computers do the same?

This problem is very easy for people to understand, but no system has yet been implemented that can solve it in such an intuitive way.

Some of the deepest and greatest insights in reasoning have been made using mathematics. It’s not surprising therefore that emulating such powerful reasoning on machines – and particularly the way humans use diagrams to ‘see’ an explanation for mathematical theorems – is one of the aims of artificial intelligence.

Diagrams for reasoning

Drawing pictures and using diagrams to represent a concept is perhaps one of the oldest vehicles of human communication. In mathematics, the use of diagrams to prove theorems has a rich history: as just one example, Pythagoras’ Theorem has yielded several diagrammatic proofs in the 2500 years following his contribution to mathematics, including that of Leonardo Da Vinci’s. These diagrammatic proofs are so clear, elegant and intuitive that with little help even a child can understand them.

The concept of the ‘mutilated’ checkerboard is another useful demonstration of how intuitive human reasoning can be used to solve problems. If we remove two diagonally opposite corners, can the board still be covered with dominoes (rectangles made out of two squares)? The elegant solution is to colour the checkerboard with alternative black and white squares, like the chessboard, and do the same with the dominoes so that a domino is made of one white and one black square. The solution then immediately becomes clear: there are more white squares than black squares, and so the mutilated checkerboard cannot be covered with dominoes. This problem is very easy for people to understand, but no system has yet been implemented that can solve it in such an intuitive way.

As these reasoning techniques can be incredibly powerful, wouldn’t it be exciting if a system could learn such diagrammatic operations automatically? So far, few automated systems have attempted to benefit from their power by imitating them. One explanation might be that we don’t yet have a deep understanding of informal techniques and how humans use them in problem solving. To advance the state of the art of automated reasoning systems, some of these informal human reasoning techniques might have to be integrated with the proven successful formal techniques, such as different types of logic.

From intuition to automation

There are two approaches to the difficult problem of automating reasoning. The first is cognitive, which aims to devise and experiment with models of human cognition. The second is computational – attempting to build computational systems that model part of human reasoning.

Steps along the computational approach are being taken by Dr Mateja Jamnik in the Computer Laboratory with funding for an Advanced Research Fellowship from the Engineering and Physical Sciences Research Council (EPSRC). While at the University of Edinburgh, Dr Jamnik built Diamond, a program that uses diagrammatic reasoning to prove mathematical concepts. However, there are theorems like the mutilated checkerboard that might require a combination of symbolic and diagrammatic reasoning steps to prove them. In Cambridge, Dr Jamnik is now investigating how a system could automatically reason about such ‘heterogeneous’ proofs. This requires combining diagrammatic reasoning in Diamond with symbolic problem solving in an existing state-of-the-art automated theorem prover. The way forward is to give heterogeneous reasoning frameworks access to intelligent search facilities in the hope that the system will not only find new and more intuitive solutions to known problems, but perhaps also find new and interesting problems.

Automated diagrammatic reasoning could be the key to making computer reasoning systems more powerful, as well as to providing the necessary tools to study and explore the nature of human reasoning. We might then have a new means to investigate the amazing ability of the human brain to solve problems.

For more information, please contact the author Dr Mateja Jamnik (Mateja.Jamnik@cl.cam.ac.uk) at the Computer Laboratory.

This work is licensed under a Creative Commons Licence. If you use this content on your site please link back to this page.