The aim of this project is to develop an understanding of what makes one diagrammatic proof more “readable” than another, and to apply that understanding in diagrammatic tools.
To begin unpacking that last sentence, whenever we use the word “readable” we ought to explain what we mean by it. Readability is, in general, a subjective quality and a matter of taste of course. I think you’d be right to be deeply sceptical of an algorithm to identify readability in fiction, for instance. Fortunately, we’re talking about formal proofs, where each step of the proof is generated from the ones that went before it according to a limited set of proof rules. For each (true) theorem, there are infinitely many proofs, each of them formally equivalent. From among those proofs, we want to find ones which users find easier to understand and there are some straightforward ways in which that can be measured — for instance, we could say that one proof, P, is more readable than another, Q, if users can identify which rules are applied in each step in P, but they are less able to do that for Q. The length of time it takes a user to read and understand a proof is part of readability too.
There is a rich history of logical diagrams, reaching back to Leibniz. In recent years, there has been a lot of interest in logical diagrams as a way to enable non-logicians to make precise statements, for instance when producing conceptual models such as ontologies. Our project focusses on Euler diagrams because they are well-known and many people find them easy to understand. This is the kind of theorem you can state and prove using Euler diagrams:
Euler diagrams themselves aren’t expressive enough for conceptual modelling tasks but more expressive systems that extend Euler diagrams software exist, such as spider diagrams and concept diagrams. So, if we can understand readability in Euler diagrams, we have a good chance of understanding it in systems that are expressive enough for real-world tasks too.
Another good reason to choose Euler diagrams is that there are already software reasoning tools, or theorem provers, that work with them. Theorem provers are either automated (enter a theorem and the tool generates a proof, if one exists) or interactive (enter the theorem then choose which rule or tactic should be applied next). EDITH is an automated Euler diagram theorem prover developed by our colleagues Gem Stapleton, Jean Flower and others at the Visual Modelling Group. Speedith, an interactive spider diagram prover, is a descendant of EDITH. We are planning to produce a version of Speedith that, like its predecessor, works automatically and do generates proofs with readability and the human reader in mind. We’re calling it Readith 🙂