-Diagrammatic notations and reasoning have become a prominent focus of research over the last two decades. We have now reached a point where the techniques required to formalize diagrammatic logics and prove meta-level results, such as soundness and completeness, are well understood. Moreover, we have insight into what makes effective diagrams. However, the majority of progress has been on diagrammatic logics that are very limited in expressiveness. Whilst such logics are exemplars of the current state-of-the-art and are useful in simple cases, they have not yet realized their full potential in real world applications. This paper summarizes the existing state-of-theart in diagrammatic logics and poses a set of open questions. The paper will discuss the need for software tools to support the creation and use of diagrammatic logics which are needed for large-scale real-world take-up. Significant research is still necessary to deliver the full potential of diagrammatic logics.
Diagrammatic notations are widely used to convey
information, reflecting their perceived benefits as a mode of
communication. In mathematics, diagrams are often sketched
as accompaniments to proofs or definitions, say, in order to
illuminate their more formal presentation. However, the
traditional presentation of formal or rigorous mathematics and, in
particular, logic has used symbolic notations that are textual in
style. In the case of logic, a mature branch of mathematics, the
long held approach to formalization is to distinguish between
the syntax and semantics. For classical logic, the semantics
are typically defined using a model-theoretic approach. This
then raises the question as to whether diagrams can be used
as an equally formal alternative to symbolic logics. This was
answered affirmatively by Shin, in seminal work during the
1990s [
Around the same time as Shin’s seminal work, Hammer
devised a sound and complete Euler diagram logic which had
just three inference rules [
Our knowledge about how to formalize diagrammatic
logics has, since those early days of Shin’s seminal contributions,
considerably advanced. Typically, they are formally defined via
an abstract syntax [
Expressiveness Diagrammatic logics should be suitably expressive for intended application domains. Inference Systems It should be possible to reason with the diagrammatic logic, to ensure that desirable properties follow from axioms defined, and that undesirable properties do not.
Manual Diagram Drawing To be practically applicable on a real-world scale, intelligent software must be provided that allows end-users to create and use diagrammatic statements.
Automated Diagram Drawing Software should be provided to automatically draw the results of inference rule applications, or translations from other notations.
All of the above need to have a strong emphasis on usability. If we are to realize a major goal of diagrams research (to provide accessible ways representing, and reasoning about, knowledge) then empirical evaluations are essential. The remainder of this paper is devoted to discussing these five aspects of diagrams research. Sections II to V correspond to the four areas listed above. Each of these sections briefly describes the existing state-of-the-art for the family of Euler diagram logics, highlights limitations and presents avenues for future work. Section VI concludes.
Most of the existing diagrammatic logics have very limited
expressiveness and are, therefore, not usable in a wealth of
real-world applications. Of the Euler diagram family, most
of them are monadic logics and cannot, therefore, talk about
relationships between elements [
We now give a set of examples to illustrate differences between these levels of expressiveness. Consider the following sentences from the given symbolic logics: (1) (2) (3) (4) (5)
DSOL[=]: 8x8y9f ((A(x) ^ f (x; y)) ) B(y)).
MFOL: 8x:(A(x) ^ B(x)) ^ 9yA(y).
MFOL[=]: 8x(A(x) , B(x)) ^ 9y9z(A(y) ^ A(z) ^ :(y = z)).
DMFFOOLL[[=]]:: 88xx8(Ay(((xA)(,x) B^(Rx()x);^y9))y9)z(BA((yy)))^. :A(z) ^ y < z).
The first sentence can be expressed by all of the diagrammatic logics in table I. Examples of an Euler diagram and a Venn-II diagram expressing the same information are in Figs 1 and 2 respectively. The Euler diagram expresses ∀x¬(A(x)∧B(x)) by using two non-overlapping closed curves (one for A and one for B). However, asserting ∃yA(y) needs to be done indirectly, by turning the statement into ¬∀y¬A(y). The statement ∀y¬A(y) is expressed by the righthand Euler diagram with the shading denoting that no elements can be in A. A horizontal bar, over the diagram, expresses negation. By contrast, the Venn-II diagram expressing (1) is more succinct, not requiring the use of any logical operators. This diagram expresses ∀x¬(A(x) ∧ B(x)) by the use of shading. The ⊗sequence asserts ∃yA(y). In fact, the part of the ⊗-sequence inside both A and B is redundant, because we know no elements are inside both A and B, because of the shading. Fig. 1. Euler diagram for (1).
A spider diagram expressing (2) is in Fig. 3. It uses graphs (here, each graph comprises a single node) to represent the existence of elements, with distinct graphs representing distinct elements. Unlike spider diagrams, Euler/Venn diagrams do not include notation for explicitly representing the existence of elements. However, Euler/Venn diagrams do include notation to represent specific elements, i.e. constants, as do spider diagrams with constants. The Euler/Venn diagram in Fig. 4 expresses ∀x¬(A(x) ∧ B(x)) ∧ A(tom) ∧ B(jerry). A spider diagram with constants expressing the same information is almost identical, shown in Fig. 5. Whilst it might appear that the inclusion of constants increases expressive power, this is actually not true. It can readily be shown that constants can be removed from logics, replacing them with existentially quantified formulae, without reducing expressiveness. See [18] for details in the case of spider diagrams with constants. Of note is that an extension of Shin’s Venn logic includes constants, but its level of expressiveness is unknown [21], [22].
Statement (3) can be expressed by a spider diagram of order, introduced by Delaney [19], [23]. This variant of the spider diagram syntax expresses ordering information by augmenting the graphs (dots) with numbers [24], as well as a ‘product’ operator between diagrams. Numbers are placed on the nodes of graphs to indicate the relative ordering of the elements represented. The diagram corresponding to (3) is in Fig. 6, where the numbering, 1, of the dot inside A (and B) tells us that the represented element is ordered before the dot, numbered 2, outside A (and B). For this example, the product operator is not needed; see [19] for details and examples of its use.
Fig. 6. Spider diagram Fig. 7. Constraint di- Fig. 8. of order for (3). agram for (4). for (5).
Concept diagram
So far, all of the example diagrams given have been from monadic languages. They all use closed curves to represent sets (corresponding to 1-place predicates in MFOL) and, except for Euler diagrams, have explicit syntax to represent elements (sometimes unnamed elements, sometimes particular elements i.e. constants). Constraint diagrams and concept diagrams both build on this level of expressiveness, by including arrows to represent properties of binary relations. For example, the constraint diagram in Fig. 7 represents the same information as statement (4). The graph whose nodes are asterisks acts as a universal quantifier over A (as it is placed inside the curve labelled A). Thus, this graph can be thought of as representing all elements in A. The arrow, then, tells us that each of these elements is related only to elements in the set represented by the target of the arrow. In this example, the target is an unnamed subset of B. To summarize, every element in A is related to only elements in B under R.
Concept diagrams are similar to constraint diagrams except that they utilize quantifiers explicitly. The example in Fig. 8 represents statement (5). Here we see the use of a ‘quantification expression’, namely ‘for all a ∈ A’, written outside of the diagram’s bounding box. Within this bounding box are two sub-diagrams. By placing the curves A and B inside different rectangles, concept diagrams avoid making assertions about the disjointness or subset relationships between the represented sets; see [25] for a discussion on how the use of multiple rectangles allows concept diagrams to reduce clutter and overcome over-specificity problems that commonly arise in diagrammatic notations.
Thus far, we have briefly detailed the expressiveness of a variety of diagrammatic logics based on Euler diagrams. There are various avenues of future work and here we pose three important open questions:
Q1: Q2: Q3:
How can Euler diagram logics be extended to represent relations of arbitrary arity? Can higher-order statements be effectively expressed by diagrammatic logics? How effective are statements made in diagrammatic logics relative to those made in symbolic logics? Does any relative benefit decrease/increase as expressiveness increases?
Q3, in particular, represents a substantial programme of research and requires many empirical studies to be conducted. The results of such studies will be greatly illuminating and, potentially, help with the development of new diagrammatic logics. Q3 will also provide evidence (or otherwise) that serves to promote the use of diagrammatic approaches in place of their symbolic counterparts. Moreover, answers to these questions will aid with the application of diagrams to solving real-world problems. For instance, in the area of software modelling, for which constraint diagrams were proposed, there can be a need to make higher-order assertions, such as to define the transitive closer of a predicate or to quantify over sets.
At the heart of any logic is its inference system. Indeed,
a key aim of the diagrammatic reasoning community is to
make proofs more accessible than those written using symbolic
logics. For the purposes of this paper, a (formal) proof is
a sequence of formulae where each formula is an axiom or
derived, using an inference rule, from formulae written down
earlier in the proof. Thus, in order to produce diagrammatic
proofs, inference rules need to be developed for diagrammatic
logics. Table II summarizes the state-of-the-art results for the
development of inference systems for logics based on Euler
diagrams. As the table indicates, the majority of the monadic
logics are associated with a sound and complete inference
system. Constraint diagrams, which we have seen include dyadic
(2-place) predicates, whilst incomplete as a logic, does have
sound and complete fragments such as [26]. The completeness
proof strategies for all these logics rely on the decidability
of the logics in question. Even though they are decidable,
obtaining completeness is not always straightforward [
We now look, in more detail, at the inference rules that have
been developed for a selection of these logics, starting with
Venn-II. Shin’s work on Venn-II (and Venn-I) [
Examples of trivial deductions, like d4, requiring nontrivial proofs are not unusual and certainly not confined to Venn-II. We now give a further, much more extreme, example of a trivial deduction requiring a non-trivial proof in the spider diagram logic. The proof task requires the deduction of d′1 ∧d2 from the assumption d1 ∧ d2 shown in Fig. 11. We observe, from d1 and d2, the following information: d1: d2:
D is a subset of B (2).
Using (1) and (2), we can readily deduce D is a subset of B ∩
C. The only difference between d1 and d′1 is the inclusion of
the information that D ⊆ B ∩ C. Intuitively, therefore, we see
d1 ∧d2 d′1 ∧d2. The natural question then arises: how can we
use spider diagram inference rules to prove d1 ∧ d2 ⊢ d′1 ∧ d2?
A proof certainly exists because the logic is complete, but all
proofs of d′1 ∧ d2 are surprisingly long. One proof strategy is
(loosely), to first add D to d1 and then manipulate the syntax
until we obtain d′ . Using the inference rules in [
The first step adds D, given in the first row of Fig. 12. The ‘add contour’ rule (the closed curves are called contours in spider diagrams) splits all regions, called zones, into two pieces. The graphs, which are called spiders, have twice the number of nodes after the rule has been applied. For each node in the original diagram, the two new nodes are placed in the two zones arising from the zone containing the original node. Semantically, this is because the element represented by the spider must lie either inside (the set denoted by) D or outside D. The proof must now use the information contained within d3 and d2 to ‘move’ D so that it is inside both B and C.
The next step is to apply a rule called excluded middle to d3. This rule turns d3 into a disjunction, with one new spider placed inside D, but outside B, to give d4 and shading is added to the same region to give d5. It is possible to show that d4 and d2 are in contradiction. Only one rule in the spider diagram logic allows contradictions to be identified and it requires that all spiders comprise single nodes, which is not the case for d4. The proof will, later, identify this contradiction. Furthermore, we can also see that, in d5, the element represented by the spider in A cannot also be in D, given the information in d2. We can apply a rule called splitting spiders to d5, giving d6 and d7 shown in the next line, turning this spider into two spiders, one inside A − D (in d6) and one inside A∩ D (in d7). As with d4 and d2, we now have d7 and d2 in contradiction. Again, the proof will eliminate this contradiction.
At this point in the proof, we now focus d6. A spider diagram inference rule that allows the removal of shaded zones that contain no spiders can be applied, five times, removing the five such zones inside D. This moves D to inside both B and C, resulting in d′ . Our diagram, at this stage in the proof, is 1 now (d4 ∨ d′1 ∨ d7) ∧ d2. To be able to identify that d4 ∧ d2 and d7 ∧ d2 are contradictions, we require all spiders to comprise just one node. We could now apply the splitting spiders rule to reduce the number of feet per spider, but this would result in an overly long proof. Instead, we remove information from d4 and d7 until only that needed for the contradiction to exist remains. For space reasons we omit the details, but the rest of the key steps in the proof are shown in Fig. 12. This 24 step proof is the shortest that we have been able to find that shows d1 ∧ d2 ⊢ d′1 ∧ d2. Clearly, for such an intuitively obvious result, this proof is not desirable.
One might ask why the proofs that arise using
diagrammatic logics are not ideal given that a key ambition is to
provide logics that are more accessible than their symbolic
counterparts? The answer lies in the reason for which the
inference rules were devised. Certainly in the case of spider
diagrams, the inference rules were designed for obtaining a sound
and complete system [
It is posited that the time is right for changing this focus, by designing inference rules that allow observable deductions to be made when writing proofs. Very recent work began, for spider diagrams, with this change of emphasis in mind [32]. New inference rules in [32] allow d′1 ∧ d2 to be proved from d1 ∧d2 in a single step, using the observable information about D in d2 to add D to d1. However, there is still a long way to go for this new approach to designing inference rule to result in improved logics, with the system in [32] only including five new rules all of which apply to diagrams of the form d1 ∧ d2.
What constitutes a readable/understandable diagrammatic proof? How can inference rules for diagrammatic logics be designed so that they enable the production of readable/understandable proofs? Are the inference rules that allow the production of readable/understandable proofs also those that best allow proofs to be written by people? Is is possible to produce a sound and complete set of inference rules that allow readable/understandable diagrammatic proofs to be written?
As with the open problems given for expressiveness questions, these challenges will require contributions from cognitive science and need many empirical studies to be executed. As it stands, there is very little understanding about how to best design diagrammatic logics when aiming to make them effective tools for people to use. Defining such logics is important if they are to realize their full potential.
IV.
If diagrammatic logics are to be useful in practice on a
wide scale, such as in the area of ontology development [33],
[
We argue that such dedicated software for diagrammatic logics should support (at least) the following: (a) (b) (c) (d) (e)
Sketch-based diagram drawing, using stylus-based input.
Diagram drawing using traditional point-and-click mouse based input.
Automatic understanding of the diagram syntax (both the concrete syntax and the abstract syntax).
Automated and interactive theorem proving support.
Automated diagram layout.
We now briefly discuss the first three requirements with respect to manual diagram drawing. The last two requirements will be discussed in the next section.
Concerning (a), sketching tools have the advantage of providing natural interaction with the diagram and aid problem solving and communication [35]. Non-sketched diagrams (sometimes called formal diagrams, i.e. those created using traditional approaches) also have a role to play, in part because of the perception that sketches are incomplete, unfinished or inaccurate in some way [36]. In addition, the formal diagram is generally required for distribution. This supports our position that intelligent diagram creation systems should support visualization via formal diagrams, which appear as though they have been drawn in an editing tool rather than by hand, as well as sketched diagrams.
The provision of such tools requires sketch recognition technology to be developed for diagrammatic logics. Early work, by WAng et al., focused on Euler diagrams [37], and has been extended to include graphs (i.e. to spider-like diagrams) by Stapleton et al. [38]. An example can be seen in Fig. 13, which shows two screenshots of the SketchSet software [37]. The top image shows a manually drawn spider diagram which has been automatically converted to the formal diagram underneath. The interface also shows a stylized version of the abstract syntax (bottom left panels in each screenshot). The tool automatically computes the abstract syntax and uses it to ensure consistency between the sketch and formal diagrams. SketchSet allows edits to be made in each interface, automatically updating the other whilst maintaining consistency. Of note is that SketchSet utilizes a single-stroke recognizer to classify the sketched diagrammatic elements.
Future challenges include answering the following questions:
Q8: Q9: Q10:
Can sketch recognition technology be developed to allow multi-stroke recognition and stroke segmentation (when one stroke contributes to two or more syntactic elements) for diagrammatic logics? What constitutes good user interface design for diagram creation tools that are specifically for diagrammatic logics? Can we produce computationally efficient algorithms for computing the abstract syntax of concrete diagrams, building on initial work for Euler and spider diagrams [37], [39], [40]? The first of these challenges is a core problem faced by the sketch recognition community. Solving it will be important if diagram creation tools are to be able to handle the variety of ways in which people draw diagrams using a stylus.
In order to fully support interactive [41] and automated theorem proving [42], diagrams need to be automatically drawn on the application of an inference rule. For some inference rule applications, automatically drawing the resulting diagram is trivial, particularly if the inference rule merely deletes an item of syntax. However, some inference rules do not give rise to simple changes in diagram syntax. For instance, in Fig. 9, the diagram d3 is not obtained from d1 or d2 by simple syntax deletion. Instead, it needs to be drawn using a more sophisticated approach. For this, algorithms are needed that automatically draw diagrams.
To-date, there has been considerable research effort towards
automatically drawing Euler diagrams [43], [
Fig. 14. An automatically drawn Euler diagram [52].
Whilst recognizable geometric shapes are desirable, and
circles are known to be both preferable [53] and most
effective [55], not all diagrams can be drawn with them. Thus, other
methods which allow arbitrary shaped curves, such as [
In order to produce the most effective diagram layouts,
shape is not the only property that must be considered. To-date,
empirical studies have been conducted exploring the impact
of layout features on the comprehension of Euler diagrams.
For instance, Blake et al. established that diagram orientation
does not impact on user comprehension [56]. Related work by
Benoy and Rodgers, showed that curves should be smooth and,
when they intersect, they should diverge and zones should have
roughly equal areas [57]. Other research has shown that
wellformed Euler diagrams (see [54] for a list of well-formedness
properties), better support comprehension than those which are
not well-formed [58]. Some layout methods aim to produce
well-formed diagrams only, such as the first ever method by
Flower and Howse [
There are still a number of very challenging research problems to be solved in this area. Here we identify those we see as the most fundamental: Q11: Q12: Q13: Q14:
How can we automatically draw diagrams that augment Euler diagrams with additional syntax? What are desirable/undesirable geometric and topological properties of logical diagrams, in terms of user comprehension and preference? Building on Q11 and Q12, how can we automatically draw diagrams for ‘best’ user comprehension? How can we automatically draw a set of diagrams that have common syntax?
For Q11, a naive approach is to automatically draw an Euler diagram and then add to it any additional syntax. However, as Fig 15 demonstrates, the best layout for the augmented diagrams need not be obtained in this way. On the left, the Euler diagram layout has compromised the addition of the graph whereas the layout on the right does not. Even partial solutions to Q12 will be able to inform layout choices, like that just illustrated, which will be key for answering Q13. Fig. 15. Layout choices: impact on syntax.
Fig. 16. Layout choices: in the context of logical connectives.
Q14 is particularly important for diagrammatic logics. For instance, a diagram that involves logical connectives could include diagrams with common parts, as in Fig. 16. Here, the common curves in d1 and d2 (namely A, B, C and D) adopt the same layout, rather than occupying significantly different positions as in d1 ∧ d3.
The only work, of which we are aware, that considers multiple Euler diagram layout (Q14) is by Rodgers et al. [59]. This work alters the layout of one diagram until it is similar to another. However, this approach is somewhat limited since it does not alter topological properties of diagrams. This means, for instance, that zone adjacency will never be altered. Thus, there are some pairs of diagrams that could both include Venn4 as a sub-diagram that will never be made to look similar using the methods of [59]. More sophisticated approaches are needed for multiple diagram layout.
VI.
This paper has summarized key results in diagrammatic logics research from a number of perspectives, focusing on expressiveness, inference, manual diagram drawing and automated diagram drawing. Whilst significant progress has been made, a number of open problems of some significance remain. We have presented some of these problems in this paper.
It is posited that solving these problems should not be done in isolation, but they should be informed by each other. Results achievable in one area will, no doubt, impact on the possible solutions in other areas. For instance, in the context of automated or interactive reasoning, the choice of inference rule application at each step could be guided by the automated layout algorithms that exist for the diagrammatic logic: the application of one inference rule may result in an ineffective layout for the resulting diagram, whereas another inference rule may yield an effective diagram layout. Optimizing proof readability and understandability will have to take into account results for diagram drawability.
Diagrams