Delivering the Potential of Diagrammatic Logics Gem Stapleton University of Brighton Email: g.e.stapleton@brighton.ac.uk Abstract—Diagrammatic notations and reasoning have be- examples of diagrammatic logics include Peirce’s existential come a prominent focus of research over the last two decades. graphs [8], further developed by both Shin [9] and Dau [10]. We have now reached a point where the techniques required to formalize diagrammatic logics and prove meta-level results, such Our knowledge about how to formalize diagrammatic log- as soundness and completeness, are well understood. Moreover, ics has, since those early days of Shin’s seminal contributions, we have insight into what makes effective diagrams. However, the considerably advanced. Typically, they are formally defined via majority of progress has been on diagrammatic logics that are an abstract syntax [11] and given a model theoretic semantics. very limited in expressiveness. Whilst such logics are exemplars Using an abstract syntax was found to overcome problems, of the current state-of-the-art and are useful in simple cases, identified by di Luzio [12], associated with attempting to they have not yet realized their full potential in real world reason about the logic at the concrete syntax level [13] (i.e., applications. This paper summarizes the existing state-of-the- reasoning with the actual drawn diagrams). Formalized and art in diagrammatic logics and poses a set of open questions. The paper will discuss the need for software tools to support well-supported diagrammatic logics with appropriate levels of the creation and use of diagrammatic logics which are needed expressiveness for real-world applications are well beyond the for large-scale real-world take-up. Significant research is still current state of the art. This is a substantial hinderance to necessary to deliver the full potential of diagrammatic logics. realizing the significant potential of diagrammatic logics and needs to be addressed. In order to address this limitation, consideration needs to be given as to what scientific advances are necessary given how such diagrams might be applied. It I. I NTRODUCTION is posited that the following are key areas that should be the Diagrammatic notations are widely used to convey in- focus of research, developed in tandem rather than in isolation, formation, reflecting their perceived benefits as a mode of to deliver this potential: communication. In mathematics, diagrams are often sketched 1) Expressiveness Diagrammatic logics should be suit- as accompaniments to proofs or definitions, say, in order to ably expressive for intended application domains. illuminate their more formal presentation. However, the tradi- 2) Inference Systems It should be possible to reason tional presentation of formal or rigorous mathematics and, in with the diagrammatic logic, to ensure that desirable particular, logic has used symbolic notations that are textual in properties follow from axioms defined, and that un- style. In the case of logic, a mature branch of mathematics, the desirable properties do not. long held approach to formalization is to distinguish between 3) Manual Diagram Drawing To be practically appli- the syntax and semantics. For classical logic, the semantics cable on a real-world scale, intelligent software must are typically defined using a model-theoretic approach. This be provided that allows end-users to create and use then raises the question as to whether diagrams can be used diagrammatic statements. as an equally formal alternative to symbolic logics. This was 4) Automated Diagram Drawing Software should be answered affirmatively by Shin, in seminal work during the provided to automatically draw the results of in- 1990s [1], who not only formalized the syntax and semantics ference rule applications, or translations from other of the Venn-I and Venn-II logics, but also provided them with notations. sound and complete inferences rules. Shin demonstrated that the syntax and semantics of diagrammatic notations can be All of the above need to have a strong emphasis on usability. If defined just as rigorously as for symbolic logics. we are to realize a major goal of diagrams research (to provide accessible ways representing, and reasoning about, knowledge) Around the same time as Shin’s seminal work, Hammer then empirical evaluations are essential. The remainder of devised a sound and complete Euler diagram logic which had this paper is devoted to discussing these five aspects of just three inference rules [2]. The last two decades have seen diagrams research. Sections II to V correspond to the four many more diagrammatic logics successfully developed. Euler areas listed above. Each of these sections briefly describes the diagrams, in particular, have been prominent in diagrammatic existing state-of-the-art for the family of Euler diagram logics, logics research, providing the basis for Swoboda and Allwein’s highlights limitations and presents avenues for future work. Euler/Venn diagrams [3], Howse et al.’s spider diagrams [4], Section VI concludes. and Kent’s constraint diagrams [5]. Moreover, Euler diagrams themselves have been investigated as a basis for syllogistic II. E XPRESSIVENESS reasoning by Mineshima et al. [6]. Indeed, it has been shown, by Sato et al., that Euler diagrams lead to better understanding Most of the existing diagrammatic logics have very limited and ability to carry out inference tasks than symbolic ap- expressiveness and are, therefore, not usable in a wealth of proaches [7]. Thus, it is undeniable that Euler diagrams have real-world applications. Of the Euler diagram family, most formed a major component of research in this field. Other key of them are monadic logics and cannot, therefore, talk about 1 relationships between elements [1], [4], [14], [15]. Some to represent specific elements, i.e. constants, as do spider extensions, such as Kent’s constraint diagrams [5], formalized diagrams with constants. The Euler/Venn diagram in Fig. 4 in [16], go beyond the monadic case, by using arrows to expresses ∀x¬(A(x) ∧ B(x)) ∧ A(tom) ∧ B(jerry). A spider represent binary relations. Concept diagrams take the level of diagram with constants expressing the same information is expressiveness beyond first-order, allowing quantification over almost identical, shown in Fig. 5. Whilst it might appear sets, elements, and binary relations [17]. Table I summarizes that the inclusion of constants increases expressive power, this the expressiveness of the family of Euler diagram-based logics, is actually not true. It can readily be shown that constants where: MFOL is monadic first-order logic, MFOL[=] is MFOL can be removed from logics, replacing them with existentially with equality, MFOL[≤] is MFOL with an order operator, quantified formulae, without reducing expressiveness. See [18] DFOL[=] is dyadic FOL with equality, and DSOL[=] is dyadic for details in the case of spider diagrams with constants. second-order logic with equality . Of note is that an extension of Shin’s Venn logic includes constants, but its level of expressiveness is unknown [21], [22]. TABLE I. T HE EXPRESSIVENESS OF E ULER DIAGRAM - BASED LOGICS Diagrammatic Logic Lower Bound Upper Bound Euler diagrams, as in [14] MFOL MFOL Venn-II, as in [1] MFOL MFOL Euler/Venn, as in [3] MFOL MFOL[=] Spider diagrams, as in [15] MFOL[=] MFOL[=] Spider diagrams with constants, as in [18] MFOL[=] MFOL[=] Spider diagrams of order, as in [19] MFOL[≤] MFOL[≤] Constraint diagrams, as in [16] >MFOL[=] DFOL[=] Fig. 3. Spider diagram Fig. 4. An Euler/Venn Fig. 5. A spider dia- Generalized constraint diagrams, as in [20] DFOL[=]