Visual logics based on Euler diagrams have recently been developed, including generalized constraint diagrams and concept diagrams. Establishing the metatheories of these logics includes providing completeness proofs where possible. Completeness has been established for such logics, including Euler diagrams, spider diagrams and a fragment of the constraint diagram logic. In this paper, we identify commonality in their completeness proof strategies, showing how, as expressiveness increases, the strategy readily extends. We identify a fragment of concept diagrams and demonstrate that the completeness proof strategy does not extend to this fragment. Thus, we have established that the existing completeness proof strategies are limited. Consequently, we examine the challenge of devising new approaches to proving completeness in more expressive logics.
There has been a lot of recent interest in logics that, in various ways, extend Euler
diagrams. This interest was sparked by pioneering work in the mid 1990s, by
Hammer [
One reason that signi cant emphasis has been placed on deriving completeness results for logics is that completeness means that the logic is capable of proving all theorems expressible within the logic. Formally, a theorem is a statement that semantically follows from a set of statements formulated in the logic, called axioms. In the case of diagrammatic logics, the set of axioms is a set of diagrams and a theorem is a diagram whose informational content is derivable from the axioms. For a theorem to be provable from the axioms, we need to be 3rd International Workshop on Euler Diagrams, July 2, 2012, Canterbury, UK. Copyright c 2012 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors. able to apply so-called inference rules, which are (informally) transformations that alter the syntax of the axioms, until we obtain the theorem.
This paper has two key parts. First, in section 2, we will demonstrate that there are substantial similarities in existing completeness proof strategies for Euler-based diagrammatic logics, with the result that we can consider the strategies to be variations on a single approach. In section 3 we describe the task of extending the proof strategy to a fragment of concept diagrams and show that the strategy breaks down. We examine the factors whose interaction prevents the ready extension of the strategy and show that completeness proofs for more expressive notations will require a di erent approach. We conclude in section 4 by describing some of the approaches that may be taken to nding suitable new strategies. 2
Completeness Strategies for Euler Diagram Logics
There have been a number of sound and complete logics based on Euler diagrams
developed to date. All of the proofs of completeness have used constructive
strategies, providing a proof that the theorem follows from the axioms (in fact,
those strategies we demonstrate are restricted to a single axiom). Moreover, they
all adopt a similar framework, converting the diagrams involved into normal
forms that are easily comparable. As we shall demonstrate in this section, the
completeness proof for each considered logic is an extension of the completeness
proofs for its fragments. We show this by detailing the strategies used for a
hierarchy of increasingly expressive logics: Euler diagrams [
Euler diagrams, as investigated by Hammer [
Hammer's logic contains just three inference rules: Erasure (of a curve), Introduction of a New Curve, and Weakening which allows new regions to be added; Weakening is illustrated in gure 1, where d + AC is obtained from d by adding a region inside both A and C. To prove completeness of this logic, Hammer proceeds by constructing a proof-writing algorithm: given an axiom d and a theorem d0, carry out the following steps to prove d0 follows from d:
each curve label, L, in d0 that is not in d, to give a diagram dc. 2. Apply the Erasure rule, erasing all curves from dc that have labels not appearing in d0, to give a diagram de. 3. Apply the Weakening rule, adding minimal regions to de until it is the same as d0.
The proof of completeness involves showing that it is possible to apply this algorithm whenever d d0 (i.e. d semantically entails d0), thus establishing that d ` d0 (i.e. there is a proof that d0 follows from d). We observe that the rst step of this proof can be considered as kind of maximising step: syntax is added to the axiom that is used in the theorem. The last step of the proof also adds syntax. In fact, we can interchange the last two steps without signi cantly impacting the details of the completeness proof. Thus, if we add minimal regions before erasing curves we would genuinely have maximised the syntax in the axiom diagram so that only inference steps that erase syntax are required in order to obtain d0. In what follows, we denote the maximised version of d by dmax , and we have, instead: 1. Apply the Introduction of a New Curve rule, adding one curve labelled L for each curve label, L, in d0 that is not in d, to give a diagram dc; we can similarly obtain d0c, which we will use to determine inference rule applications at the next step. 2. Apply the Weakening rule, adding minimal regions to dw until it has the same the same minimal regions as d0c, to obtain dw = dmax , the maximised version of d. 3. Apply the Erasure rule, erasing all curves from dmax that have labels not appearing in d0, to give a diagram de. Then de = d0.
That is, we have:
d ` dc ` dw = dmax ` de = d0: To determine which minimal regions to add to obtain dmax , we constructed a diagram, d0c from d0 by adding the curves with labels that occur in d but not in d0. Then dc and d0c have the same curve labels, so the minimal regions are immediately comparable; we add regions that are in d0c but are not in dc, thus maximising the syntax to get dmax . As we shall see, this concept of maximising the syntax in the axiom diagram is a recurring theme in subsequently developed completeness proofs. The completeness proof strategy is illustrated in gure 2, where we show d ` d0.
In order to illustrate the extension of this strategy to more expressive systems, including spider diagrams in the next subsection, we formalize the notion of maximal forms. First, we de ne an (abstract) Euler diagram: De nition 1. An Euler diagram is a pair, d = (L; R), where L is a nite set of curve labels and R f(in; L in) : in Lg is a nite set of regions. So, d in gure 2 is, formally, d = (L; R) where L = fA; B; C; Dg and
R = f(;; fA; B; C; Dg); (fAg; fB; C; Dg); (fA; Bg; fC; Dg); (fCg; fA; B; Dg); (fC; Dg; fA; Bg)g: For example, (fAg; fB; C; Dg) corresponds to the region inside the curve labelled A but outside the curves labelled B, C, and D1.
Now, going back to the completeness proof strategy, we have seen that dmax is created by constructing the diagram d0c which does not formally comprise part of the proof that d ` d0; in gure 2 we have dmax = d0c when d ` d0. We de ne the maximal form as follows: De nition 2. Let dc = (L; R) and d0c = (L0; R0) be Euler diagrams such that L = L0. The diagram dc is maximal with respect to d0c provided R0 R.
It can be shown, given that dc is maximal with respect to d0c, d d0c if and only if R = R0. In terms of the completeness proof strategy, this means that dmax = d0c. Our re-ordering of the steps in Hammer's completeness proof can now be informally justi ed. Firstly, to dc we add precisely the minimal regions in d0c that are not in dc to give dw = dmax . Since d0c is semantically equivalent to d0 and d0c = dmax , it should be easy to see that we can then merely delete curves from dmax to give d0, establishing completeness. 1 The elements of R are often called zones but in this paper we call them regions for consistency with Hammer's work.
Spider diagrams extend the Euler diagram logic of Hammer in two distinct ways:
they are augmented with (a) trees, called spiders, and shading, both of which are
used within diagrams to place constraints on set cardinality, and (b) logical
connectives which are used to allow more complex expressions to be formed. Whilst
Euler diagrams form a very simple monadic rst-order logic, spider diagrams
take the level of expressiveness to monadic rst-order logic with equality [
Examples of spider diagrams can be seen in gure 3 where, in addition to the information provided by the underlying Euler diagram, d1 expresses { using spiders { that there are at least two elements, one of which is in B and the other of which is in B [ D. Diagram d1 also expresses { using shading { that no further elements are in B. Here, each of the spiders (one of which comprises a single node) represents the existence of an element. The shading in a region, r, expresses that all elements in the set represented by r must be represented by spiders. The spider diagram d2 _ d3 is semantically equivalent to d1.
The completeness proof strategy for spider diagrams, from [
Since the rules applied to convert to normal forms are equivalences, we see that if it can be shown that dNF ` d0NF , then we have established d ` dNF ` d0NF ` d0: We focus on the part of the completeness proof that establishes dNF ` d0NF . Since dNF is in normal form, by de nition this means that dNF =
∨ 1 i n
di; d0NF =
∨
1 i m
d0 :
i
where each di is a unitary spider diagram containing only spiders that are single
nodes. Similarly,
Returning to our consideration of regions, these normal forms ensure that, for
each di and d0j in dNF and d0NF respectively, the sets of regions are the same.
That is, if we consider the underlying Euler diagrams, Li = L0j and Ri = R0 .
j
So, the `Euler part' of di is maximal with regard to the `Euler part' of dj and
we have the right `Euler conditions' for semantic entailment (i.e. if there were
no spiders or shading then di ` d0j ). What remains is to consider the e ects
of spiders and shading. By comparing dNF and d0NF , an inference rule can be
applied to dNF in order to add spiders and shading to its components, increasing
the number of diagrams in the disjunction, until it can be established that each
unitary diagram, di, in the axiom logically entails a unitary diagram, d0j , in
the theorem. In this sense, the completeness proof strategy for spider diagrams
maximizes the syntax in the axiom by adding curves (to get the `right' curve
label set), adding regions, and nally adding spiders and shading. Similar to the
Euler diagram case, once this maximal form is achieved it is merely a matter of
erasing syntax from di to obtain d0j . We have di ` d0NF (by using an inference
rule analogous to P ` P _ Q in propositional logic). Subsequently, it can be
trivially shown that dNF ` d0NF , as required. We refer to [
For our purposes, it is su cient for us to now de ne unitary spider diagrams where spiders comprise only single nodes, and to extend the de nition of maximal to this case.
De nition 3. A spider diagram is a tuple, d = (L; R; R ; S; ), where (L; R) is an Euler diagram, R R is a set of shaded regions, S is a nite set whose elements are called spiders and : S ! R is a function that identi es the region in which each spider is placed.
In gure 3, the spider diagram d2 has d of gure 2 as its underlying Euler diagram for which we previously speci ed L and R. In addition, there is one shaded region, and we have R = f(fA; Bg; fC; Dg)g, two spiders, so S = fs1; s2g, and these spiders are placed in regions as given by (s1) = (fA; Bg; fC; Dg) and (s2) = (fC; Dg; fA; Bg). For diagrams with spiders comprising single nodes, the de nition of maximal is as follows: De nition 4. Let d = (L; R; R ; S; ) and d0 = (L0; R0; R 0; S0; 0) be spider diagrams such that L = L0. The diagram d is maximal with respect to d0 provided R0 = R, R 0 R and there exists an injection, f : S0 ! S such that for each s0 2 S0, 0(s0) = (f (s0)).
The de nition of maximal given for spider diagrams generalizes that for Euler
diagrams2. Intuitively, our de nition of maximal is saying that everything that
occurs in d0 also occurs in d. The next lemma follows from a similar result in [
Theorem 1. Let d = (L; R; R ; S; ) and d0 = (L0; R0; R 0; S0; 0) be spider diagrams such that L = L0 and R = R0. If d is maximal with respect to d0 and d d0 then d ` d0.
Proof (Sketch). By lemma 1, each region that is shaded in d0 contains the same number of spiders in d. Thus we can erase shading from d until R = R 0, obtaining di, then remove spiders from di, that are not mapped to by the injective function f : S(d0) ! S(d). Finally, rename the spiders to obtain d0. Theorem 2. Let d = (L; R; R ; S; ) and d0 = (L0; R0; R 0; S0; 0) be spider diagrams such that L = L0 and R = R0. If d d0 then d is maximal with respect to d0.
Proof (Sketch). The proof is by contradiction. Suppose d d0 but d is not maximal with respect to d0. Then either R 0 6 R or there is no suitable injection, f , from the spiders of d0 to those of d. In the rst case, d0 contains a shaded region, r, which is non-shaded in d. Then d0 asserts that the set represented by r contains exactly n elements, where n is the number of spiders in r in d0. However, d allows the set represented by r to contain n + 1 elements, so d 6 d0. In the second case, where there is no suitable injection, f , there is a region, r0, in d0 that contains more spiders than in d. Here, d asserts that the set represented by r0 contains at least n elements, where n is the number of spiders in r0 in d. However, d0 asserts that the set represented by r0 contains at least n+j elements, where j is the number of `extra' spiders in r0 in d0. Again, d 6 d0. Thus, since d d0, the conditions for maximality must be satis ed.
We now have a completeness result concerning the fragment of the spider diagram logic that we have de ned: Theorem 3 (Completeness). Let d = (L; R; R ; S; ) and d0 = (L0; R0; R 0; S0; 0) be spider diagrams such that L = L0 and R = R0. If d d0 then d ` d0.
d0 then, by theorem 2, d is maximal with respect to d0. By theo
rem 1, d ` d0.
To summarize, whilst the overall strategy is more complex, we still have a process of adding syntax to the axiom in order to maximize it with respect to the theorem we are aiming to prove. 2 Note that for Euler diagrams we stipulated R0 R, but for spider diagrams we have R = R0. This di erence is not signi cant; it merely makes the details of our argument more straightforward. 2.3
Constraint diagrams build on spider diagrams by adding further syntax, in
particular arrows, to place constraints on binary relations. The system developed
in [
First, to give a brief introduction to the meaning of arrows, consider d in gure 4. The arrow labelled g tells us that (the element represented by) the spider at its source is related to precisely the elements in C, the target, under (the relation represented by) g. Similarly, the spider in D is related to the unique element in B under f , and no other elements. In this example, d is maximal with respect to both d0 and d00. Here, d d0 but d 6 d00. In the case of d and d0, we can injectively map the spiders from d0 to d in such a manner that the regions in which they are placed match. That is, there is an injective function f : S0 ! S where (s0) = (f (s0)) and f ensures that the induced function g : A0 ! A is also an injection, where A0 and A are the sets of arrows for d0 and d respectively. Arrows are of the form (label ; source; target ) and g(l; s; t) = (l; f (s); f (t)) in the case where s and t are both spiders. We then delete shading, along with spiders and arrows that are not mapped to by f and g, from d to obtain d0.
Similar functions exist for d and d00, but this time we cannot apply inference
rules to erase syntax from d to give d00. We would need to erase a spider from
a shaded region, which is not sound; as with spider diagrams, the numbers of
spiders in the shaded regions of the theorem, d0, must match those in the axiom,
d. Similarly to the spider diagram case, the number of spiders in the shaded
regions of the theorem must be the same as in the axiom. These examples give
the idea of the maximal forms used in constraint diagrams. We refer the reader
to [
We now consider extending the proof strategy described in the previous section
to concept diagrams, which are intended to be used to model ontologies; see [
The diagram in gure 5 is a concept diagram. The part of the diagram made up of labelled curves, shading and spiders is a spider diagram. The arrows provide information about binary relations. The diagram d expresses the following, in addition to the information given in the underlying spider diagram: 1. there are two sets, x and y, the former is a subset of A and the latter is a subset of C, 2. the image of the relation f , when its domain is restricted to y, is A, 3. there is an element, a, in A x such that the image of the relation g, when its domain is restricted to a, is the element in C y.
We now present the syntax of the fragment of concept diagrams under
consideration, adapted from [
De nition 5. A unitary concept diagram is a tuple d = (L; C; R; R ; S; ; A), where 1. L = L(d) is a nite set whose elements are called labelled curves, 2. C = C(d) is a nite set whose elements are called anonymous curves, 3. R = R(d) is a set of regions such that
R f(in; (L [ C) in) : in
L [ Cg: 4. R = R (d) R is a set of shaded regions. 5. S = S(d) is a nite set whose elements are called spiders, 6. = d : S ! R is a function that returns the location of each spider. 7. A = A(d) is a nite set of arrows, each of the form (l; s; t), where l is the label, s 2 L [ C is the source and t 2 S [ L [ C is the target.
If d = (L; C; R; R ; S; ; A) is a concept diagram and C = ; then ds = (L; R; R ; S; ) is a spider diagram. Semantics are assigned to concept diagrams similarly to the previous notations discussed: in addition to the usual interpretation of the underlying spider diagram, the arrows of a concept diagram place restrictions on binary relations and the anonymous curves represent the existence of sets as illustrated in our examples3.
In order to extend the strategy discussed in the previous section to concept diagrams, we rst extend the de nition of maximality: De nition 6. Let d = (L; C; R; R ; S; ; A) and d0 = (L0; C0; R0; R 0; S0; 0; A) be concept diagrams such that L = L0. The diagram d is maximal with respect to d0 provided: 1. there exists a bijection g : L0 [ C0 ! L [ C such that (a) g is the identify map when its domain is restricted to L0, (b) g induces a bijection h : R0 ! R, de ned by h(in; out ) = (in0; out 0), where i. in0 = fg(c0) : c 2 ing, and ii. out 0 = fg(c0) : c0 2 out g, which ensures for each (in; out ) 2 R 0, h(in; out ) 2 R , 2. there exists an injection, f : S0 ! S such that for each s0 2 S0, 0(s0) = (f (s0)), and 3. g and f induce an injection p : A0 ! A de ned by p(l; s; t) = (l; g(s); g(t)) if s; t 2 L0 [ C0 (l; g(s); f (t)) if s 2 L0 [ C0 ^ t 2 S0 (l; f (s); g(t)) if s 2 S0 ^ t 2 L0 [ C0 (l; f (s); f (t)) if s; t 2 S0:
Equipped with the de nition of maximality, we can examine how to generalize the lemma and theorems from section 2.2 in order to extend the strategy. We start by considering the equivalent of lemma 1: Conjecture 1. Let d = (L; C; R; R ; S; ; A) and d0 = (L0; C0; R0; R 0; S0; 0; A0) be concept diagrams such that L = L0. Suppose d is maximal with respect to d0. Then d d0 if and only if for each shaded region, r0, in R 0, the number of spiders in r0 is the same as the number of spiders in h(r0) in d.
Figure 6 shows a counterexample to conjecture 1. First, it is obvious that d1 is maximal with respect to d2. Here, d1 tells us that there exists a set containing exactly two elements. From this we can deduce that there exists a set containing exactly one element. That is, d2 follows logically from d1. The shaded region in d2 contains fewer spiders than in d1. In both these diagrams, we see that the shading is actually redundant: removing the shading does not alter the informational content of the diagrams. 3 Here, we note that our representation of concept diagrams assumes that spiders represent the existence of elements; strictly, in concept diagrams, spiders act as free variables. Formally, unitary diagrams as we have de ned them would need to be pre xed by existential quanti es (one for each spider) to get our interpretation. However, to avoid diagram clutter, we simply omit the existential quanti ers since no ambiguity arises.
Clearly, such problems concerning spiders and shading impact our ability to obtain a completeness result for the fragment under consideration. In order to obtain completeness, we need inference rules that allow us to identify when (a) shading is redundant, (b) we can delete spiders from shaded regions, and (c) when anonymous curves are redundant. Worthy of note is that the diagrams in gure 6 are semantically equivalent to spider diagrams (on removing the anonymous curves, the informational content is unaltered). Thus, the problems here arise from the syntactic richness of the notation and are not merely because of an increase in expressive power.
To proceed with our exposition of problems that arise when attempting to extend the previously used proof strategies to concept diagrams, we extend the de nition of maximal to incorporate the condition on shading given in conjecture 1:
By doing this, we are following the standard mathematical process of applying further constraints to a conjecture for which we have found a counterexample. In fact, conjecture 1 is trivially true in the strongly maximal case. As a consequence, our attempts to extend the completeness strategy apply to a smaller fragment of concept diagrams.
Next, we consider extending theorem 1 to concept diagrams: Conjecture 2. Let d = (L; C; R; R ; S; ; A) and d0 = (L0; C0; R0; R 0; S0; 0; A0) be concept diagrams such that L = L0. If d is strongly maximal with respect to d0 and d d0 then d ` d0.
To establish the truth of conjecture 2, we start by de ning the inference rules which are needed to establish d ` d0, if d is strongly maximal with respect to d0 and d d0.
Inference rule 1: Remove arrow. Let d = (L; C; R; R ; S; ; A) be a concept diagram and let a 2 A be an arrow in d. Let d0 = (L; C; R; R ; S; ; A fag) be the diagram obtained by removing a from d. Then d logically entails d0. Inference rule 2: Remove shading. Let d = (L; C; R; R ; S; ; A) be a concept diagram and let r 2 R be a shaded region in d. Let d0 = (L; C; R; R fr g; S; ; A) be the diagram obtained by removing the shading from r in d. Then d logically entails d0.
Inference rule 3: Remove spider. Let d = (L; C; R; R ; S; ; A) be a concept diagram and let x 2 S be a spider with an non-shaded location in d. Let d0 = (L; C; R; R ; S fxg; ; A) be the diagram obtained by removing x from d. Then d logically entails d0.
Inference rule 4: Substitute spider Let d = (L; C; R; R ; S; ; A) be a concept diagram and let x 2 S. Let y be a spider not in S. Let d0 = (L; C; R; R ; (S fxg) [ fyg; ( f(x; (x)g) [ f(y; (x)g; A) be the diagram obtained by replacing x with y in d1. Then d is logically equivalent d0.
Inference rule 5: Substitute anonymous curve Let d = (L; C; R; R ; S; ; A) be a concept diagram and let c 2 C. Let c0 be an anonymous curve not in C. Let d0 be the diagram obtained from d by replacing all occurrences of c with c0. Then d is logically equivalent d0.
We have su cient inference rules to show that conjecture 2 is true. Theorem 4. Let d = (L; C; R; R ; S; ; A) and d0 = (L0; C0; R0; R 0; S0; 0; A0) be concept diagrams such that L = L0. If d is strongly maximal with respect to d0 and d d0 then d ` d0.
Proof (Sketch). Assume d is strongly maximal with respect to d0. By the definition of strong maximality there is an injection, p, from the arrows of d0 to the arrows of d. Therefore, we can apply rule 1, remove arrow, to d until its arrows match those of d0, i.e. p becomes bijective. Similarly, we can apply rule 2, remove shading, repeatedly until the shading of d matches that of d0. Now, by the de nition of strong maximality, each shaded region, r0, in d0, contains the same number of spiders as h(r0) in d. This means we can apply rule 3 to remove spiders until f is bijective. All that di ers now are the spiders and the anonymous curves. Apply rules 4 and 5 to obtain d0.
We must now consider whether theorem 2 extends to concept diagrams: Conjecture 3. Let d = (L; C; R; R ; S; ; A) and d0 = (L0; C0; R0; R 0; S0; 0; A0) be concept diagrams such that L = L0. If d d0 then d is strongly maximal with respect to d0.
Figure 6 provides a counterexample to conjecture 3 (as well as conjecture 1). The problems arising from counterexamples like gure 6 may be easy to overcome (by de ning inference rules that remove redundant anonymous curves, for instance). We will now demonstrate that problems also arise in more complex situations where arrows are involved.
Such a counterexample to conjecture 3 can be seen in gure 7. In d, the anonymous curves x and y are given labels for convenience. The arrow (f; A; B) tells us the image of f when its domain is restricted to A is B. One of the elements inside x is related to nothing under f , which we know by the arrow targeting the curve that represents the empty set (i.e. the curve containing shading but no spiders). At least one of the other elements inside A must therefore be related to the element inside B. In d0, the arrows provide this information that we have just deduced from the arrows of d. The other information provided by d0 `agrees' with that provided by d, so d d0. However, d is not strongly maximal with respect to d0: there is no appropriate injective mapping from arrows of d0 to those of d.
As stated above, with regard to shading and spiders we can attempt to overcome the problems by devising inference rules for removing redundant anonymous curves, for example. With regard to arrows, the question arises as to whether we can add arrows to diagram d, gure 7, until there is an appropriate injection from the arrows of d0 to those of d. This leads to the notion of potential arrows, those arrows which can be added to a diagram without changing its meaning: De nition 8. Let d = (L; C; R; R ; S; ; A) be a concept diagram and let a 62 A be an arrow not in d. Let d0 = (L; C; R; R ; S; ; A [ fag). If d is semantically equivalent to d0 then a is a potential arrow for d.
In gure 7, there are two potential arrows for d. The arrow (f; A; B) tells us that at least one element of A is related under f to the element in B, and so we can add an arrow which represents this information explicitly. The arrows (f; x; B) in diagram d1 and (f; y; B) in diagram d2, gure 8, are potential arrows for d, since either arrow can be added to d without changing its meaning. After adding either arrow, however, the other arrow ceases to be a potential arrow. Neither d1 nor d2 have any potential arrows. Thus, an element of choice arises when adding potential arrows to concept diagrams, which again causes problems for completeness. Rather, adding potential arrows results in a set of obtainable diagrams each of which is semantically equivalent to the original diagram. In gure 8, fd1; d2g is the set of such diagrams obtainable from d ( gure 7).
If we are to extend the completeness proof strategy by adding arrows to the axiom, all of the diagrams obtained from d using this process must have an arrow set that can be injectively mapped to by the arrows of d0 in the appropriate way; this is because the diagrams obtained are semantically equivalent to d and, therefore, semantically entail d0. We can see that we can remove syntax from d2 to obtain d0 since d2 is strongly maximal with respect to d0. However , there is currently no sequence of rules that would, or general strategy that can be used to, transform d1 into d0, even though d1 d0 (since d1 is semantically equivalent to d and d d0); d1 is not strongly maximal with respect to d0.
A possible approach to overcome this problem is to determine whether we can remove syntax from d0 without changing its meaning until we have an appropriate injection from its arrows to those of, in this example, d1. Unfortunately, no arrows can be removed from d0 without weakening information, so such an approach is still insu cient.
Compared to the steps required to extend the de nition of maximality, the non-uniqueness of the ways in which we can add arrows is the most serious blow so far to the aim of extending the completeness proof strategy. It is not at all clear how we need to change the syntax of an arbitrary axiom, d, to obtain d0 in general. As we have demonstrated, we need to devise strategies for altering the spiders, shading and the arrows present in either the axiom and/or theorem until the axiom is strongly maximal with respect to the theorem. Even once this is solved, it will be challenging to extend the completeness proof strategies to larger fragments of the concept diagram logic. 4
We have identi ed commonality in the completeness proof strategies of various logics based on Euler diagrams and shown how, as expressiveness increases, the strategy readily extends in some cases. We have illustrated various ways in which this strategy breaks down for concept diagrams, which are syntactically richer and more expressive than earlier logics based on Euler diagrams. The problems identi ed with extending the completeness strategy to concept diagrams arise because we cannot simply delete syntax from the axiom to obtain the theorem, even for the very small fragment that we considered. Thus, we have established that the existing completeness proof strategies are limited. The non-unique ways of adding syntax to concept diagrams, which further complicates the issue, results from the syntactic richness of the notation and from their expressive power. We believe that the same phenomena will arise in equally expressive logics.
We examined ways in which parts of the completeness proof strategy might be `patched up' but we conjecture that a new strategy needs to be developed. One (rather undesirable) route to obtaining completeness for fragments of concept diagrams is to derive inference rules for them inspired by complete symbolic logics4. This is not the route we want to pursue, strongly preferring a set of inference rules that makes use of diagrammatic reasoning. Even small fragments of the more expressive visual logics will require new completeness strategies.
We believe the need for expressive visual logics such as concept diagrams is clear, since they allow the techniques of diagrammatic reasoning to be applied in new domains, such as ontology speci cation. For these logics to be fully exploited, we need to develop sound inference rules with clearly understood metatheories, including establishing expressiveness and identifying complete fragments. Understanding the e ect that increases in both syntactic richness and notational expressiveness have on completeness is essential for the informed design of new logics. 4 Symbolic logics have radically di erent (uncomparable) completeness proof strategies due to their vastly di erent syntax.