Next Article in Journal
Cloud Gamification: Bibliometric Analysis and Research Advances
Previous Article in Journal
SWAR: A Deep Multi-Model Ensemble Forecast Method with Spatial Grid and 2-D Time Structure Adaptability for Sea Level Pressure
Previous Article in Special Issue
Extensions of the Maximum Bichromatic Separating Rectangle Problem
 
 
Font Type:
Arial Georgia Verdana
Font Size:
Aa Aa Aa
Line Spacing:
Column Width:
Background:
Article

Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion, and Transfer Axioms under Simple Transformations

Faculty of Computer Science, Universitiy of Koblenz-Landau, 56070 Koblenz, Germany
*
Author to whom correspondence should be addressed.
Information 2022, 13(12), 578; https://doi.org/10.3390/info13120578
Submission received: 31 July 2022 / Revised: 28 November 2022 / Accepted: 1 December 2022 / Published: 12 December 2022
(This article belongs to the Special Issue Advances in Discrete and Computational Geometry)

Abstract

:
We study classes of geometric graphs, which all correspond to the following structural characteristic. For each instance of a vertex set drawn from a universe of possible vertices, each pair of vertices is either required to be connected, forbidden to be connected, or existence or non-existence of an edge is undetermined. The conditions which require or forbid edges are universally quantified predicates defined over the vertex pair, and optionally over existence or non-existence of another edge originating at the vertex pair. We consider further a set of simple graph transformations, where the existence of an edge between two vertices is logically determined by the existence or non-existence of directed edges between both vertices in the original graph. We derive and prove the correctness of a logical expression, which is a necessary and sufficient condition for containedness relations between graph classes that are described this way. We apply the expression on classes of geometric graphs, which are used as theoretical wireless network graph models. The models are constructed from three base class types and intersection combinations of them, with some considered directly and some considered as symmetrized variants using two of the simple graph transformations. Our study then goes systematically over all possible graph classes resulting from those base classes and all possible simple graph transformations. We derive automatically containedness relations between those graph classes. Moreover, in those cases where containedness does not hold, we provide automatically derived counter examples.

1. Introduction

In this paper, we study, for a specific type of axiomatically described graph, how to prove containedness between geometric graph classes automatically. The term graph class here means a collection of graphs that satisfy the same property. Specifically, a geometric graph class refers to graphs with vertices drawn in the Euclidean space, or more generally, in a metric space. Given two graph classes, proving containedness refers to checking whether one class is contained in the other, i.e., any graph from one class is also a valid graph in the other class.
The studied method to prove containedness is illustrated with simple geometric graph models used in the theoretical wireless network research. The method in general is applicable to any geometric graph class, which can be described using a class of axioms containing inclusion conditions, which enforce the existence of an edge between two vertices, exclusion conditions, which prohibit the existence of an edge between two vertices and transfer conditions, which enforce the existence of edges between two vertices depending on the existence of other edges originating from the two vertices to be connected. The axioms depend on properties of the two vertices (inclusion; exclusion) or the three vertices (transfer) but not on the remaining vertices of the vertex set. For any two vertices where neither an edge is enforced or prohibited by the inclusion, exclusion, or transfer conditions, we are free to choose to connect them by an edge or not.
In addition to the graph classes themselves, we also examine graph transformations on graph classes. A transformation is a mapping that constructs a new graph from a given graph on the basis of logical rules applied on edge and vertex properties. More specifically, we consider transformations on graph classes, which we call simple. A simple transformation maps a source graph on an image graph with the same vertex set. The existence or nonexistence of an edge between two vertices in the image graph depends on the existence or nonexistence of the two possible edges between the two vertices in the source graph. Such dependencies can be described using Boolean expressions with two variables.
This work is an extension of our previous work [1], where we studied, with symmetric subgraph and symmetric supergraph, two specific simple transformations. In general, with two edges either existing or not existing, there are 16 simple transformations. In this work, we define those 16 transformations and systematically study all of them by automatically proving containedness relations between all possible classes resulting from specific inclusion, exclusion and transfer axioms and all possible transformations applied on these classes. More precisely, given two graph classes A , B , which can be described using inclusion, exclusion, and transfer axioms, let C = γ 1 ( A ) and D = γ 2 ( B ) be the classes obtained by applying the simple graph transformations, γ 1 and γ 2 . We test automatically whether class C is contained in class D . The test yields satisfiability if the subclass relation C D holds. Otherwise, if not, the test yields a vertex minimal example graph, which is contained in C but not in D .
The studied problem is not trivial. On the one hand, the predicates used for enforcing resp. prohibiting edges can be themselves formulas in a complex theory (in which properties or norms, costs or distances need to be specified). On the other hand, consider the question whether a class C is contained in a class D = γ 2 ( B ) obtained from class B after applying a (simple) transformation γ 2 . To answer this question, one would typically need to demonstrate that for every graph H in class C , there exists a graph G in class B , such that H = γ 2 ( G ) , or to give an example of a graph H in C , such that for every graph G in B , we have H γ 2 ( G ) . A naive logical encoding of such properties would require quantification over binary relations. In order to avoid these problems, in this paper we demonstrate how expressions (involving only the predicates for enforcing and prohibiting edges and for transfer) for testing containedness between graph classes can be generated in a systematic way. For this, we prove a small model theorem. Our results can be regarded as a form of second-order quantifier elimination [2,3].
In summary, the contributions of this work are: (1) We systematically describe geometric wireless network graph classes on the basis of so-called inclusion, exclusion, and transfer predicates. (2) By means of the so-called simple graph transformations applied on these classes, we cover additional graph classes, with some of them also considered to describe geometric wireless network graphs. (3) We derive a logical formula to automatically verify whether one of such graph clasess described by inclusion, exclusion, and transfer predicates and simple graph transformations is contained in another one or not. (4) The result is used to systematically investigate all possible containedness relations of the so-defined classes, demonstrating all possible combinations in a table at the end of this paper. (5) Finally, for those pairs of classes where containment does not hold, an automatically generated minimal counter example is provided.
The remainder of the paper is structured as follows. In the next section, we illustrate the concept of the considered graph classes and transformations with an example referring to graph models used in theoretical wireless network research. In Section 3, we formally introduce the terminology, in particular, notions such as inclusion, exclusion and transfer axioms and graph classes defined with these types of axioms, as well as the notion of simple transformations. In Section 4, we propose a method of generating finite axiomatizations for a class γ ( C ) , which do not refer to the edges of graphs in C . Furthermore, we prove a small model theorem (i.e., we demonstrate that searching for a counter example with at most four vertices is sufficient for checking containedness relations for the graph classes and transformations that we study in this paper). We use this for reducing subclass relationship tests to check the satisfiability of expressions (built in a systematic way), which do not refer to the edges of the graphs but only to the inclusion, exclusion and transfer predicates used in the description of the classes. Based on these results, we demonstrate in Section 5 how containedness relations can be proved for the 128 possible graph classes resulting from the examples discussed in Section 2. We conclude this contribution in Section 6 and discuss future research directions on extending the concept of logical graph class definitions and the concept of logical described transformations. The paper is accompanied with three appendices. Appendices Appendix A and Appendix B demonstrate an automatically derived table of the containedness relations between all 128 possible graph classes, as well as the automatically found minimal graph examples for those cases where containedness does not hold. Appendix C finally provides a longer proof for a technical lemma used for the axiomatization of the studied graph transformations.

2. Geometric Graph Models

We illustrate our theory with graph models applied in the theoretical wireless network research. Initial theoretical studies modeled such networks as unit disk graphs  UDG , where network vertices are connected if their Euclidean distance is less or equal than 1 and vertices are not connected by self-loops. The model was extended in several directions. We consider the extensions quasi units disk graphs [4,5] and directed transmission graphs [6,7,8] (Note, we consider a maximum communication distance of 1. This is no limitation to other work, where a maximum communication distance r > 0 is used instead. Obviously, scaling vertex positions with 1 / r yields the same model with maximum communication distance 1).
Quasi unit disk graphs QUDG ( r ) have a maximum distance 1 and a minimum distance 0 < r 1 . Two distinct vertices with a Euclidean distance less or equal r are always connected. Two vertices with Euclidean distance greater than 1 are never connected. Any other vertex pairs can be but do not have to be connected. To our knowledge, quasi unit disk graphs have only been studied as undirected graphs. We assume here as well that they are undirected graphs when we speak of quasi unit disk graphs.
With directed transmission graphs DTG ( r ) , every vertex v has an individual maximum communication distance r ( v ) r for some general r > 0 . A directed edge exists from v to w if the distance between v and w is less or equal to r ( v ) . Directed transmission graphs can be made symmetric by removing all directed edges where the reverse edge is missing, as described in [6,9] or by adding the missing reverse edges, as it is additionally considered in [6]. We denote these graphs by DTG ( r ) and DTG ( r ) + , respectively.
In the following, we describe the defining properties of the discussed graph models in terms of three base graph classes and the two discussed basic graph transformations, i.e., either removing directed edges where the reverse edge is missing or adding the missing reverse edges.
Definition 1 
(The classes CRG , MinDG , MaxDG ). Let 0 < r 1 . We consider a graph G = ( V , E ) . Let d ( u , v ) be any metric defined on the vertices (e.g., Euclidean distance when vertices are located in the Euclidean space). Let E ( u , v ) be true if u v E and false ; otherwise, graph G is in the class of min disk graphs MinDG ( r ) , max disk graphs MaxDG ( r ) , or connected region graphs CRG if it satisfies the following corresponding conditions:
MinDG ( r ) u , v V : u v d ( u , v ) r E ( u , v ) MaxDG ( r ) u , v V : d ( u , v ) > r ¬ E ( u , v ) CRG u , v , w V : E ( u , w ) u v d ( u , v ) d ( u , w ) E ( u , v )
Definition 2 
(Symmetric super and subgraph). Given a graph G = ( V , E ) , the graph transformations G + = ( V , E + ) and G = ( V , E ) , denoted as symmetric supergraph and symmetric subgraph, respectively, are defined by:
E + = { u v : u v E or v u E } E = { u v : u v E and v u E }
When applied on a whole graph class C , we write C γ , which means that the transformation γ is applied on each graph contained in C .
Obviously, the graph class of unit disk graphs can be built from the defined base classes, as follows
UDG = MinDG ( 1 ) MaxDG ( 1 )
where intersection ∩ means that the graph is contained in both classes, or expressed alternatively, has to satisfy the logical predicates of both classes.
Together with the two basic graph transformations, the class of quasi unit disk graphs [4,5] is given by
QUDG ( r ) = ( MinDG ( r ) MaxDG ( 1 ) ) = ( MinDG ( r ) MaxDG ( 1 ) ) +
The latter equality holds, since an edge u v is optional if v u is optional, i.e., r < d ( u , v ) = d ( v , u ) 1 . Obviously, QUDG ( 1 ) is the special case of unit disk graphs UDG .
The class of directed transmission graphs [6,7,8] is given by
DTG ( r ) = MaxDG ( r ) CRG
This is followed immediately by setting the individual maximum communication distance of vertex v to r ( v ) = max { d ( v , w ) : v w E } . The symmetric variant considered in [9] has no maximum communication distance and is obtained by removing all directed edges where the reverse edge is missing. It is thus described by CRG . The symmetric variants considered in [6] are DTG ( r ) and DTG ( r ) + in our graph class notation.

3. Axiomatic Description of Graph Classes

3.1. Inclusion, Exclusion, and Transfer Predicates

Generally speaking, in the motivating example, we consider graph classes C , where each graph G = ( V , E ) consists of vertices V of a vertex universe Ω and an edge relation E, which satisfies
u , v V : π C i ( u , v ) E ( u , v )
u , v V : π C e ( u , v ) ¬ E ( u , v )
u , v , w V : E ( u , w ) π C t ( u , v , w ) E ( u , v )
u , v , w V : ¬ E ( u , w ) π C t ( u , w , v ) ¬ E ( u , v )
We term π C i ( u , v ) , π C e ( u , v ) and π C t ( u , v , w ) inclusion, exclusion, and transfer predicates, respectively. We will refer to the Conditions (1)–(3) as inclusion, exclusion and transfer axioms, accordingly (though Conditions (3) and (4) are equivalent, we list both here for later reference).
We say that a graph G = ( V , E ) is in class C (and write G C ) if G satisfies the Conditions (1)–(3). In this case, we sometimes also write Gsatisfies class C . If the graph class C consists of all graphs satisfying a set of axioms of the form (1)–(3), we will say that C is a graph class described by inclusion, exclusion, and transfer axioms. In this work, we will study such graph classes and transformations on them. We make the following additional assumptions:
Assumption A1.
(Independence)We assume that the inclusion, exclusion and transfer predicates are determined by the properties of their arguments u , v , w V and are independent of any other vertices in V. We can ensure this, for instance, by requiring that these predicates are expressed as quantifier-free formulae over a background theory.
The inclusion, exclusion, and transfer predicates defining the classes MinDG ( r ) , MaxDG ( r ) and CRG in Section 2 can be expressed as quantifier-free formulas over a theory in which we can talk about points and distances between points:
π C i ( u , v ) : = u v d ( u , v ) r π C e ( u , v ) : = d ( u , v ) > r π C t ( u , v , w ) : = u v d ( u , v ) d ( u , w )
Assumption A2.
(Transitivity)We assume the transfer predicates π C t ( u , v , w ) to be transitive, i.e.,
π C t ( u , v , w ) π C t ( u , w , x ) π C t ( u , v , x )
Obviously, the transfer predicate defining CRG in Section 2 is transitive.
Assumption A3.
(Soundness)We assume inclusion, exclusion, and transitive transfer predicates to be sound, which means that they are not contradicting:
u , v V : π C i ( u , v ) ¬ π C e ( u , v ) u , v , w V : π C i ( u , w ) π C t ( u , v , w ) ¬ π C e ( u , v )
We term a graph class to be sound in this case.
It is easy to see, as long as r 1 r 2 any conjunction of the predicates MinDG ( r 1 ) , MaxDG ( r 2 ) and CRG defined in Section 2 satisfies the soundness condition.

3.2. Simple Graph Class Transformations

The most general form of a graph transformation γ is a mapping which transfers a given graph G into a graph H. A graph transformation applied on a graph class C results in a graph class γ ( C ) , which consists of all graphs H for which there exists a graph G C with H = γ ( G ) .
We say a graph transformation γ is vertex preserving if γ ( G ) has the same vertex set as G, i.e., given G = ( V , E ) , the transformation is γ ( G ) = ( V , F ) for some F. Obviously, a vertex preserving transformation γ on the null graph ( , ) yields the null graph.
We term a vertex preserving graph transformation simple if there exists a Boolean function in two variables δ : B 2 B (where B is the two-element Boolean algebra) such that for all graphs G = ( V , E ) the transformation γ ( G ) = ( V , F ) satisfies
u , v V : F ( u , v ) = δ ( E ( u , v ) , E ( v , u ) )
The symmetric super graph ( · ) + and symmetric subgraph ( · ) are obviously simple transformations with boolean functions ∨ and ∧, respectively. As there are 4 2 = 16 possible Boolean functions of the form δ : B 2 B , in total, there exist 16 possible vertex preserving simple graph transformations, as shown in Table 1 and Table 2.
In both tables, all four possible combinations of existence or non-existence of the edge u v and v u in the original graph is shown in the table header by the column values 0 and 1 for E ( u , v ) and E ( v , u ) . For each of those possible cases, the edge u v can be added or not added to the resulting image graph. All possible combinations are shown by the eight rows of both tables (i.e., 16 in total) by the values 0 and 1 for F ( u , v ) , where F ( u , v ) defines the existence or non-existence of the edge u v in the resulting image graph.
We define for each transformation a symbol and a mnemonic in Table 1. For each transformation in that table, the negated form can be defined, as listed in Table 2. Given a transformation γ , the negated transformation ¬ γ yields the complement graph of the graph G resulting from γ , i.e., each existing edge in G is erased and each missing edge in G is added. Specifically for the transformation empty graph G , the negated empty graph G ¬ is the complete graph, of course.
We list in the last column of Table 1 whether the transformations always yield a symmetric graph (i.e., u , v V : F ( u , v ) F ( v , u ) ), a directed graph (i.e., u , v V : F ( u , v ) ¬ F ( v , u ) ), or whether we keep that column entry empty if the image graph is neither necessarily symmetric nor directed. As shown in Table 2, the symmetry is preserved for the complementary graphs given by the negated transformations. However, the last two shown transformations yield graphs, which we term complementary directed, which means that the complement of the graph is directed.
In the following discussion, we have to distinguish between the two specific transformations xor graph G and as well negate the xor graph G ¬ and all remaining ones. It turns out that for all cases, despite these two xor ones, a small counter example with, at most, four vertices can be found if a subclass relation does not hold. For the two xor cases, this is not the case. For these two transformations, arbitrary long chains of edge dependencies to determine minimum counter examples are possible. The proof is given in Lemma 5. Only under a specific condition (as discussed later), and also for the two xor cases, proving that a subclass relation does not hold, is possible with a four vertex example.
To distinguish between those situations where all transformation are considered and where all despite the two xor cases are considered, we define for the following discussion by
Γ = { ( · ) x , ( · ) ¬ x : x = , + , , id , , , }
the set of all transformations except the two transformations G and G ¬ .

4. Proving Graph Class Containedness Relations

4.1. General Properties

As stated by the following lemmas, it is easy to see that graph classes described by inclusion, exclusion and transfer axioms, which satisfy Independence (Assumption 1), and  graph classes obtained by applying a simple transformation on such graph classes are closed under induced subgraphs (Given a graph G = ( V , E ) , the graph G induced by V V consists of vertex set V and all edges from E connecting the vertices in V ). Moreover, given a sound graph class, for each finite vertex set V, we can find an edge configuration such that the given graph class axioms are satisfied.
Lemma 1.
Let C be a graph class described by inclusion, exclusion and transfer predicates, satisfying Independence (Assumption 1). It holds:
  • The null graph ( , ) satisfies C .
  • Let G = ( V , E ) satisfy C . Every subgraph G induced by V V satisfies C .
Proof. 
Obviously V = satisfies any universally quantified condition and thus also Conditions (1)–(3).
For the second statement, consider a graph G = ( V , E ) , which satisfies C . Conditions (1)–(3) are satisfied for V. Let V V . Consider one of the conditions defining the class C , say Condition (1):
u , v : π C i ( u , v ) E ( u , v ) .
Let u , v V . Then, u , v V . Assume that π C i ( u , v ) is true (relative to the set of edges, V ). By Independence (Assumption 1), the value of this predicate is independent of the other vertices in the graph, so π C i ( u , v ) is true also when we consider the whole set of vertices in G = ( V , E ) . As G satisfies Condition (1), it follows that E ( u , v ) is true (i.e., there is an edge from u to v in G). Since E = E ( V × V ) , there is an edge from u to v also in G .
The same line of argumentation can be used for Conditions (1) and (2). This shows that also the subgraph G induced by V satisfies C .    □
Remark 1.
The first part of Lemma 1 holds for every graph class, which consists of all graphs satisfying a set of universally quantified axioms.
The second part of Lemma 1 is vacuously true if Soundness (Assumption 3) does not hold, because in this case the graph class contains only the empty graph, which does not have proper subgraphs.
If Independence (Assumption 1) is not satisfied, then the second part of Lemma 1 does not necessarily hold. Consider, for instance, the graph class C described by axioms of the form (1)–(3), where for all u , v , x :
π C i ( u , v ) = w ( ( w u w v ) ( E ( u , w ) E ( w , v ) ) ) π C e ( u , v ) = false , π C t ( u , x , v ) = false .
In this graph class, the graph G = ( { a , b , c , d , e } , { ( a , b ) , ( b , e ) , ( a , d ) , ( d , e ) } ) satisfies the Axioms (1)–(3), but the subgraph induced by V = { a , b , d , e } does not satisfy axiom (1).
Lemma 2.
Let C be a graph class defined by inclusion, exclusion and transfer predicates satisfying Independence (Assumption 1) and γ be a vertex preserving graph transformation. It holds:
  • The null graph ( , ) satisfies γ ( C ) .
  • If γ is simple and if H = ( V , F ) satisfies γ ( C ) , then every subgraph H induced by V V satisfies γ ( C ) .
Proof. 
The first statement follows immediately: ( , ) = γ ( ( , ) ) since γ is vertex preserving, and  γ ( ( , ) ) γ ( C ) since ( , ) C with Lemma 1.
For the second statement, consider a graph H = ( V , F ) , which satisfies γ ( C ) . With γ being vertex preserving, there exists a graph G = ( V , E ) C such that H = γ ( G ) . Let V V , H = ( V , F ) be the subgraph of H and G = ( V , E ) be the subgraph of G induced by V , respectively.
Let δ be the boolean function of the simple transformation γ . For all u , v V holds: u v is an edge of γ ( G ) iff
δ ( E ( u , v ) , E ( v , u ) ) δ ( E ( u , v ) , E ( v , u ) ) F ( u , v ) F ( u , v )
This implies H = γ ( G ) , and thus H γ ( C ) , since G C with Lemma 1.    □
Remark 2.
The second part of Lemma 2 does not necessarily hold if the transformation γ is not simple. Consider, for instance, the transformation defined by
u , v ϕ ( u , v ) F ( u , v ) , u , v ¬ ϕ ( u , v ) ¬ F ( u , v )
where ϕ ( u , v ) : = w ( u w v w ) ( E ( u , w ) E ( w , v ) ) .
Let C be a graph class defined by inclusion, exclusion and transfer axioms containing the graph G = ( { a , b , c , d } , { ( a , b ) , ( b , d ) } ) due to the fact that in this specific graph π C i ( a , b ) = π C i ( b , d ) = true , π C e ( x , y ) = true for all other pairs of vertices, and  π C t ( u , v , w ) is false everywhere. Then H = γ ( G ) = ( { a , b , c , d } , ) γ ( C ) . However, the subgraph H of H induced by V = { a , b , d } is not in γ ( C ) : Assume there exists a graph G C with H = γ ( G ) . Since G C , due to the fact that π C i ( a , b ) = π C i ( b , d ) = true , π C e ( x , y ) = true for all other pairs of vertices, and  π C t is false everywhere, the set of edges of G must be E = { ( a , b ) , ( b , d ) } . But then in this case w ( a w d w E ( a , w ) E ( w , d ) ) holds, so in γ ( G ) , an edge ( a , d ) should exist. However, this edge is missing in H .
Lemma 3.
Let C be a graph class defined over sound conditions (Assumption 3). For each finite set V Ω at least one graph G = ( V , E ) exists, which satisfies C .
Proof. 
Consider any such set V. Set E ( u , v ) = true if π C i ( u , v ) holds or if there exist a w V such that π C i ( u , w ) π C t ( u , v , w ) holds. Otherwise set E ( u , v ) = false . This configuration obviously Satisfies (1) and (3), and does not Contradict (2) since the conditions are sound. Thus, the such defined graph G = ( V , E ) satisfies C .    □
Note that if C is a graph class defined using inclusion, exclusion and transfer axioms and γ is a simple vertex preserving transformation, it is not immediate that γ ( C ) can also be described by inclusion, exclusion and transfer axioms.
In Section 4.2, we show that when γ Γ we can describe the properties of the edge-relation F of graphs H = ( V , F ) in γ ( C ) using axioms in which only F and the inclusion, exclusion and transfer predicates π C i ( u , v ) , π C e ( u , v ) and π C t ( u , v , w ) are used.

4.2. Axiomatization for γ ( C )

We next show the connection between edge configurations F ( u , v ) for a graph being in a class transformed by a transformation in Γ and the inclusion, exclusion and transfer predicates of that class.
Lemma 4.
Let B be a sound graph class described by inclusion, exclusion and transitive transfer predicates π B i ( u , v ) , π B e ( u , v ) , π B t ( u , v , w ) , respectively. Let γ be any of the vertex preserving, simple graph transformations in Γ. A graph H = ( V , F ) is in class γ ( B ) , if for every u , v V the edge relation F ( u , v ) satisfies the implications depicted in Table 3 for that transformation.
Proof. 
Two implication directions “⇒” and “⇐” have to be shown.
The idea of the proof is only sketched here and the detailed proof is given in the Appendix. To show the direction ⇒, we start with a graph H = ( V , F ) B γ . For each graph H there exists at least one graph G = ( V , E ) B with H = G γ . Then, the conditions for the predicates of such an graph G are derived in terms of the predicates. To show the direction ⇐, we have a graph H = ( V , F ) such that the edge inclusion and exclusion implications depicted for B γ in the according Table are satisfied. We construct a graph G = ( V , E ) such that G B and G γ = H , which then implies H B γ .    □

4.3. Minimal Counter Examples

We are interested in solving the following problem: Assume that we have two graph classes, A and B , defined by inclusion, exclusion and transfer axioms, and two transformations γ 1 and γ 2 . We are interested in checking whether γ 1 ( A ) γ 2 ( B ) .
In general, A γ ( B ) , if there exists a graph G = ( V , E ) A , which is not contained in γ ( B ) . We term such graph a witness graph. Moreover, we term G a minimum witness graph if | V | | V | for all witness graphs G = ( V , E ) . In general, a minimum witness graph is not necessarily unique.
The size of a minimum witness graph depends on the transformation γ and the transformed class B . As summarized in the next theorem, for the simple vertex preserving transformations in Γ , with  Lemma 4 we obtain upper bounds on the number of vertices of a minimum witness graph. We term this value the maximum size of a minimum witness graph  μ ( γ ) .
Theorem 1.
Let γ 1 and γ 2 be any of the vertex preserving simple graph transformations in Γ. Let A and B be graph classes defined by inclusion, exclusion and transfer predicates, which satisfy Independency, Transitivity and Soundness (Assumptions 1–3). Let μ ( γ 2 ) as defined in Table 3 for transformation γ 2 . γ 1 ( A ) γ 2 ( B ) if there exists a graph G = ( V , E ) with V Ω and | V | μ ( γ 2 ) , such that G γ 1 ( A ) and G γ 2 ( B ) .
Proof. 
With γ 1 ( A ) γ 2 ( B ) follows that there exists a graph G = ( V , E ) with V Ω such that G γ 1 ( A ) and G γ 2 ( B ) . Consider such graph G = ( V , E ) , which is minimal in | V | . Assume | V | > μ ( γ 2 ) .
Since G γ 2 ( B ) , Lemma 4 implies that there exist u 1 , , u μ ( γ 2 ) , such that at least one of the expressions for F ( u , v ) or ¬ F ( u , v ) for transformation γ 2 in Table 3 is not satisfied.
Since | V | > μ ( γ 2 ) , there exists a y 0 V , which differs from u 1 , , u μ ( γ 2 ) . Consider the subgraph G induced by V { y 0 } . All edges between vertices of u 1 , , u μ ( γ 2 ) exist in G if they exist in G. Thus, at least one of the expressions for F ( u , v ) or ¬ F ( u , v ) for transformation γ 2 does also not hold for G and thus G is not contained in γ 2 ( B ) .
However, with Lemma 2 the subgraph G induced by V { y 0 } is a graph in γ 1 ( A ) . Since G was assumed to be minimal in | V | , graph G must be contained in γ 2 ( B ) (otherwise G would not be a minimum witness graph), a contradiction.    □
While for all transformations in Γ , a minimum witness graph with at most four vertecies exists, this does not hold for the two transformations ( · ) and ( · ) ¬ .
Lemma 5.
The size of the minimum witness graph for the transformations ( · ) and ( · ) ¬ is unbounded.
Proof. 
Assume the maximum size of a minimum witness graph for the transformation ( · ) is k. Consider a graph with k + 1 vertices V = { v 1 , , v k + 1 } , where all edges F ( v i , v i + 1 ) for i = { 1 , . . . , k } shall be included in the transformed graph. The predicate π A i ( v 1 , v 2 ) is true.
Furthermore, all predicates π A t ( v j , v j 1 , v j + 1 ) are true for j even and 2 j k and all predicates π A t ( v j , v j + 1 , v j 1 ) are true for j odd and 3 j k .
Then, all edges E ( v j , v j 1 ) and E ( v j , v j + 1 ) have to be set to true for j odd, while all edges E ( v j 1 , v j ) and E ( v j + 1 , v j ) have to be set to false for j odd. The case of j even is here already covered.
If the inclusion predicate π A i ( v k + 1 , v k ) is true if k is odd or the exclusion predicate π A e ( v k + 1 , a n d v k ) is true if k is even, then there is no possibility to include all edges v i v i + 1 for i = { 1 , , k } . However, if all other predicates are false, any subset of the edges v 1 , v 2 , , v k , v k + 1 can be included. Therefore, the minimum size of a maximum witness graph is k + 1 and since k was arbitrary, it is unbounded.
Analogously, the same construction yields that also the maximum size of a minimum witness graph for the negated ( · ) transformation is unbounded.    □

4.4. Expressions for Proving Subclass Relations

In this subsection, we consider different combinations of existing and non-existing edges. We provide formulas for the transformations in Γ , such that if these formulas are true, then the considered combination of existing and non-existing edges is not possible for these transformations.
A combination of these formulas in negated and the non-negated form yields an expression for checking if one graph class is contained in another one or not. If not, the expression yields axioms for a counter example.
In the Table 4 and Table 5, we only list the expressions for the non-negated transformations. The expressions for negated transformations can be obtained by changing the sets of existing and non-existing edges. With the color coding defined in Figure 1 we illustrate some of the expressions in Figure 2a,b and Figure 3.
Theorem 2.
Let γ 1 and γ 2 be two of the vertex preserving simple graph transformations in Γ. Let A and B be graph classes defined by inclusion, exclusion and transfer predicates satisfying Independence, Transitivity and Soundness (Assumptions 1–3). Let ρ γ 1 ( A ) k ( · , · ) resp. ρ γ 2 ( B ) k ( · , · ) be the expressions listed in Table 4 resp. Table 5 for γ 1 and γ 2 . Moreover, let μ ( γ 2 ) be the maximum size of a minimum witness graph as defined for γ 2 in Table 3. It holds: γ 1 ( A ) γ 2 ( B ) if there exists a graph H = ( V , F ) with | V | μ ( γ 2 ) such that
k = 1 11 ¬ ρ γ 1 ( A ) k ( S k , T k ) ρ γ 2 ( B ) k ( S k , T k )
is satisfied, where S k and T k are specific subsets S k F and T k V × V F , as defined in the Table 4 and Table 5 and V is the vertex set of H for each ρ X k ( · , · ) expression.
Proof. 
Theorem 1 states that γ 1 ( A ) γ 2 ( B ) is satisfied if there exists a counter example with a size, at most μ ( γ 2 ) .
To obtain a graph H such that H γ 1 ( A ) , but  H γ 2 ( B ) , for the expressions listed in Table 4 resp. Table 5, ρ γ 1 ( A ) k ( S k , T k ) has to be non-satisfiable, but  ρ γ 2 ( B ) k ( S k , T k ) has to be satisfiable. Hereby, G = ( V , E ) is the graph before considering the graph transformations and ρ X k ( S k , T k ) means that it is not possible to include all edges in S k , while excluding all edges in T k . Consequently, ¬ ρ X k ( S k , T k ) means that it is possible to include all edges in S k , while excluding all edges in T k .
The expressions can be derived by the conjunction of the expressions for graph class transformation X in Table 3. For the edges in S k , the expression for F ( u , v ) has to be used, while for the edges in T k the expression for ¬ F ( u , v ) has to be used. The expressions we derive in this way refer to the case that it is possible to include the edges in S k , while excluding the edges in T k and therefore yields an expression for ¬ ρ X k ( S k , T k ) . Negating ¬ ρ X k ( S k , T k ) yields the expression for ρ X k ( S k , T k ) , given in Table 4 resp. Table 5. The expressions for the negated transformations can be obtained by switching the sets S k and T k .    □
The expression of Theorem 2 simplifies significantly when testing A A + or A + A and if the predicates safisfy two additional properties called predicate-symetric and predicate-forwarding.
Definition 3.
A graph class A is called predicate-symmetric if u , v V : π A i ( u , v ) π A i ( v , u ) and π A e ( u , v ) π A e ( v , u ) holds.
Definition 4.
A graph class A is called predicate-forwarding if u , v , w V : π A i ( u , v ) π A t ( u , w , v ) π A i ( u , w ) and π A e ( u , v ) π A t ( u , v , w ) π A e ( u , w ) holds.
Obviously, predicate-symmetric and predicate-forwarding graph classes can still satisfy Independence, Transitivity and Soundness (Assumptions 1–3).
The graph classes of the application described in Section 2, are predicate–symmetric and predicate-forwarding.
Corollary 1.
Let A be a predicate–symmetric and predicate-forwarding graph class defined by inclusion, exclusion and transfer axioms, satisfying Independency, Transitivity and Soundness (Assumptions 1–3). We have: A A + iff
¬ π A e ( v , w ) ¬ π A i ( u , v ) ¬ π A i ( w , x ) π A t ( v , u , w ) π A t ( w , x , v )
and A + A iff
¬ π A i ( v , w ) ¬ π A e ( u , v ) ¬ π A e ( w , x ) π A t ( v , w , u ) π A t ( w , v , x )
is satisfied for some u , v , w , x .
Corollary 2.
For predicate–symmetric and predicate-forwarding graph classes A Theorem 2 can also be applied for the transformations A and A ¬ by using the following ρ i expressions:
ρ B 1 ( { u v } , { } , V ) = π B e ( u , v ) π B i ( u , v ) ρ B 2 ( { } , { u v } , V ) = false ρ B 3 ( { u v , v u } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 5 ( { u v } , { v u } , V ) = true ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V ) v = w ρ B 7 ( { v u } , { w u } , V ) = ρ B 1 ( { v u } , { } , V ) ρ B 2 ( { } , { w u } , V ) v = w ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V ) ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V ) ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V ) u = w v = x ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
Proof. 
We have to derive the appropriate expressions for Lemma 4 for this specific case.
If π B i ( u , v ) holds, then by the symmetry of the predicates also π B i ( v , u ) holds and then E ( u , v ) and E ( v , u ) have to be set to true . This yields ¬ F ( u , v ) . Analogously, if  π B e ( u , v ) holds, then by the symmetry of the predicates also π B e ( v , u ) holds and then E ( u , v ) and E ( v , u ) are both set to false , i.e., ¬ E ( u , v ) and ¬ E ( v , u ) holds. This also yields ¬ F ( u , v ) . Since the predicates are furthermore predicate-forwarding, predicates for other edges have no impact on the existence of the edges E ( u , v ) and E ( v , u ) . Furthermore, neither E ( u , v ) nor ¬ E ( u , v ) implies F ( u , v ) , ¬ F ( u , v ) , F ( v , u ) , ¬ F ( v , u ) . The only further condition we have to consider is the symmetry of F. Finally, this yields
F ( u , v ) F ( v , u ) ¬ π B i ( u , v ) ¬ π B e ( u , v ) ,
while no restrictions exist for ¬ F ( u , x ) .
This yields ρ B 1 ( { u v } , { } , V ) = π B e ( u , v ) π B i ( u , v ) , ρ B 2 ( { } , { u v } , V ) = false and ρ B 5 ( { u v } , { v u } , V ) = true . Due to the symmetry of the transformations, i.e., any edge u v exists if and only if edge v u exists, the reaming ρ i expressions follow identically by the method applied in Theorem 2.    □

5. Example Application

5.1. Manual Application of the Derived Concept

We first illustrate the presented concept manually by applying it to the graph classes discussed in Section 2. We use the concept to demonstrate that the class ( QUDG ( r ) ) is the same as class ( QUDG ( r ) ) + (as already discussed). Moreover, we apply the concept to show that the classes ( DTG ( r ) ) and ( DTG ( r ) ) + studied in the literature are in fact classes, with none being contained in the other one.
The inclusion predicate MinDG ( r ) and exclusion predicate MaxDG ( r ) are obviously symmetric, as long as d ( u , v ) is symmetric (which we assume for this example). The class QUDG ( r ) has an inclusion and exclusion but no transfer predicate, i.e., the transfer predicate is always false . Thus, for testing ( QUDG ( r ) ) ( QUDG ( r ) ) + and ( QUDG ( r ) ) + ( QUDG ( r ) ) , neither (7) nor (8) of Corollary 1 are satisfied. Thus, both inclusions must be satisfied, and we have in fact the equality of both graph classes.
Now, the relation between ( DTG ( r ) ) + and ( DTG ( r ) ) is considered. Applying Corollary 1 together with DTG ( r ) = MaxDG ( r ) CRG (i.e., we have only exclusion and transfer predicate) we have to check the satisfiability of
( ¬ d ( v , w ) > r ) ( v u d ( v , u ) d ( v , w ) ) ( w x d ( w , x ) d ( w , v ) )
for testing ( DTG ( r ) ) ( DTG ( r ) ) + and
( ¬ d ( v , u ) > r ) ( ¬ d ( w , x ) > r ) ( v w d ( v , w ) d ( v , u ) ) ( w v d ( w , v ) d ( w , x ) )
for testing ( DTG ( r ) ) + ( DTG ( r ) ) .
This yields the counterexample d ( v , u ) , d ( w , x ) d ( v , w ) r , u v , w x , u w and v x , which proves ( DTG ( r ) ) ( DTG ( r ) ) + . As well, this yields the counterexample d ( v , w ) d ( v , u ) , d ( w , x ) r , v w , u w and v x , which proves ( DTG ( r ) ) + ( DTG ( r ) ) . Thus, neither ( DTG ( r ) ) + nor ( DTG ( r ) ) is contained in the other class. The according counterexamples can be found in Appendix B with the examples indexed: 52 and 53.
Now let us drop the assumption of the examples in Section 2, that d ( u , v ) is a metric. Assume that d ( u , v ) = d ( v , u ) is not required. In this case, the inclusion and exclusion predicate are not necessarily symmetric. Corollary 1 is not applicable. We have to resort to the Theorem 2. The relation between ( QUDG ( r ) ) and ( QUDG ( r ) ) + is now considered again. For testing the relation ( QUDG ( r ) ) ( QUDG ) + , the second conjunction of expression (6) yields ¬ ρ A 2 ( { } , { u v } ) ρ A + 2 ( { } , { u v } ) . Replacing the formula with the predicates by using Table 4 yields ¬ π A i ( u , v ) ¬ π A i ( v , u ) π A i ( u , v ) π A i ( v , u ) = ¬ π A i ( u , v ) π A i ( v , u ) π A i ( u , v ) ¬ π A i ( v , u ) .
This formula is satisfied if d ( u , v ) < r and d ( v , u ) r or d ( u , v ) r and d ( v , u ) < r . Thus, we have found a counter example that the relation ( QUDG ( r ) ) = ( QUDG ( r ) ) + does not necessarily hold when d ( u , v ) is not a metric.

5.2. Automatically Derived Graph Class Relations

The tables in Appendix A show the automatically derived relations between all example geometric graph classes resulting from wireless networks, which we defined in Section 2. Since in this specific case the graph class axioms are predicate-symmetric and predicate-forwarding, we can also check for subclass relations, including the two xor transformations.
In case the relation does not hold, a counter example with at most four vertices can be found. We show the found counter examples in Appendix B. The counter examples are consecutively numbered and labeled with the expression ρ i (as defined by Table 4 and Table 5 and the negated forms) which led to unsatisfiability.
The tables in Appendix A are to be read from left to right as follows. Class in row i is related to class in column j according to table entry ( i , j ) , by relation:
=
The classes are the same
The class is contained in the other class but the classes are not the same
The class contains the other class but the classes are not the same
×
Neither of the two classes is contained in the others, (by lemmas 1 and 2 each of the studied graph classes contain at least the null graph. Thus, none of the considered graph classes are disjoint).
The relations ⊂, ⊃ and × in the tables are indexed with the numbered counter examples from Appendix B. Notation C n D refers to the counter example number n, which shows that D is not contained in C . Analogously, C n D refers to the counter example number n, which shows that C is not contained in D . Finally, C × n m D refers to the counter example n, which shows that C is not contained in D and the counter example m, which shows that D is not contained in C .
The class name encoding in the tables in Appendix A is as defined at the beginning of the paper, summarized by the following Hasse diagram. To avoid clutter, the tables depict the graph classes without the fixed parameters r and 1.
Class All (not defined so far) means all of the predicates (i.e., inclusion, exclusion, and transfer) are false . With all preconditions being false, all graphs satisfy inclusion, exclusion, and transfer predicate. Thus, the class just contains all graphs over the given vertex universe Ω .
Classes MinDG ( r ) , MaxDG ( 1 ) and CRG are as already defined based only on inclusion, exclusion, and transfer predicate, respectively. All the remaining classes result from the intersection of the classes, which are predecessors in the diagram (observed from the top to bottom).
The class names BG ( r ) and MDTG ( r ) were not used before. We define them here for the sake of the completeness of the tables. For graphs in class BG ( r ) (which we term boost graphs), an arbitrary long link can be added to a vertex, which boosts the connectivity of that vertex. It will be connected to all other vertices with the same or less distance. The graphs in class MDTG ( r ) (which we term minimum radius DTGs) are a DTG but also with a minimum connectivity radius, where vertices are always connected.
Opposed to the usual assumption that QUDG ( r ) actually stands for a symmetric subgraph/supergraph of MinDG ( r ) MaxDG ( 1 ) , we denote it here just as MinDG ( r ) MaxDG ( 1 ) to stay consistent with the notation used in the table. Class QUDG ( r ) , as usually used in the literature, can be found under QUDG and the same class QUDG + in the table.
The tables in Appendix A are tiled into 8 × 8 blocks, referred to as M ( γ 1 , γ 2 ) in the following, each representing the relations of the classes All , MinDG , MaxDG , CRG , QUDG , BG , DTG , and  MDTG under the transformations γ 1 and γ 2 , i.e.,  M ( γ 1 , γ 2 ) , and represents the 64 relations given by
× γ 1 ( All ) , γ 1 ( MinDG ) , γ 1 ( MaxDG ) , γ 1 ( CRG ) , γ 1 ( QUDG ) , γ 1 ( BG ) , γ 1 ( DTG ) , γ 1 ( MDTG ) × γ 2 ( All ) , γ 2 ( MinDG ) , γ 2 ( MaxDG ) , γ 2 ( CRG ) , γ 2 ( QUDG ) , γ 2 ( BG ) , γ 2 ( DTG ) , γ 2 ( MDTG )
All relations in the tables in Appendix A were automatically determined by applying FindInstance of Mathematica 12.1 on the derived expression (6) using the Euclidean metric.
In connection with the relations of the base classes shown in the Hasse diagram in Figure 4, the following observations can be made for the derived tables.
For each M ( γ , γ ) block (i.e. when applying the same transformation to the columns and rows of the block), the row for All is the row for MDTG but read reversed from right to left instead of left to right. The same applies for the row pairs ( MinDG , DTG ) , ( MaxDG , BG ) and ( CRG , QUDG ) (which are not directly connected in the Hasse diagram).
Moreover, the transformations ( · ) and ( · ) + yield obviously the same graph class when applied on All . The same applies to QUDG , as already discussed. As well, applied on MinDG and as well on MaxDG , transformations ( · ) and ( · ) + yield the same classes, respectively.
These base classes ( All , MaxDG , MinDG and QUDG ) are as well exactly those classes whose symmetric variants due to ( · ) and ( · ) + are contained in the base class. For the other classes neither the subset relation nor superset relation is satisfied between base classes and their symmetric variants.
Both transformations ( · ) and ( · ) + obviously preserve the subset relation order of the base classes. Moreover, neither ( · ) nor ( · ) + yield two base classes collapsing into one single class.
The graph class relation for all classes between directed and symmetric, complementry-directed and symmetric, and as well, directed and complementry-directed is always orthogonal, i.e., the 8 × 8 block M ( γ 1 , γ 2 ) consists only of entries × n m in this case.
Trivially, M ( , ) and M ( ¬ , ¬ ) consists only of entries =, since the first always yields the empty graph independent of the source graph, while for the latter, it is always the complete graph as well as being independent of the source graph.
Finally, putting all the tables together into one single table (with the same class ordering for rows and columns) yields a trivially symmetric matrix with diagonal entries =, however, with reversed relations ⊂ and ⊃ for all off-diagonal entries.

6. Conclusions

In this paper, we described how to prove or disprove containedness relations of specific axiomatic-described geometric graph classes on a meta-level. We proved the correctness of the general logical existentially quantified expressions over placeholders for inclusion, exclusion, and transitive transfer predicates. We illustrated the concept with concrete predicates in the context of simple theoretical wireless network models.
Though we focused on geometric classes in this work, by its generality, the concept is also applicable to any graph class, which can be described by means of inclusion, exclusion and transfer axioms and simple graph transformations.
The decidability of the problem of testing containedness for concrete inclusion, exclusion and transfer predicates depends on the concrete theories we consider. These are typically extensions of the theory of real numbers with norms, distances, cost functions or more general function symbols. In ongoing work, we are investigating the decidability of such theories.
Though a logical representation of graphs is not new in general, we believe with the axiomatic graph class representation and the discussed simple transformations described in this work, we discovered a promising graph theoretical novel concept for containedness verification, which can be generalized in many further directions.
Future work includes extending the theory beyond simple graph transformations. Moreover, one can drop the condition on transfer predicates to be transitive or even further that the edges involved do not have to be originated at the two vertices to which the transfer predicate is applied.

Author Contributions

L.B. and H.F. contributed equally to this work. All authors have read and agreed to the published version of the manuscript.

Funding

This research received no external funding.

Institutional Review Board Statement

Not applicable.

Informed Consent Statement

Not applicable.

Data Availability Statement

Not applicable.

Acknowledgments

We would like to thank for all discussions with Viorica Sofronie-Stokkermans providing us with background information on the general theory of formal verification.

Conflicts of Interest

The authors declare no conflict of interest.

Appendix A. Automatically Derived Containedness Relations

Information 13 00578 i001
Information 13 00578 i002
Information 13 00578 i003
Information 13 00578 i004
Information 13 00578 i005
Information 13 00578 i006
Information 13 00578 i007
Information 13 00578 i008

Appendix B. Automatically Derived Counter Examples

Information 13 00578 i009
Information 13 00578 i010
Information 13 00578 i011
Information 13 00578 i012
Information 13 00578 i013
Information 13 00578 i014

Appendix C. Proof of Lemma 4

Proof. 
Two implication directions “⇒” and “⇐” have to be shown.
The proof omitted in the main part is given here in the appendix.
Part 1 (⇒).
With H = ( V , F ) B γ there exists a graph G = ( V , E ) B with H = G γ . The proof is split up in two sub parts. The first part contains the proof that holds for all transformations in Γ and in the second part transformation, specific proofs are considered.
Subpart 1 (all transformations in Γ ).
If an edge is required to exist in G, i.e., E ( u , v ) , then graph class Axiom (2) implies
¬ π B e ( u , v )
Moreover, graph class Axiom (4) implies that for all x V the expression E ( u , x ) ¬ π B t ( u , x , v ) holds. Since E ( u , x ) implies ¬ π B e ( u , x ) with graph class Axiom (2), we have that
x : ¬ π B e ( u , x ) ¬ π B t ( u , x , v )
has to be satisfied.
If an edge is forbidden to exist in G, i.e., ¬ E ( u , v ) then with graph class Axiom (1), this implies
¬ π B i ( u , v )
Moreover, graph class Axiom (3) implies that for all x V the expression ¬ E ( u , x ) ¬ π B t ( u , v , x ) has to be satisfied. Since ¬ E ( u , x ) implies ¬ π B i ( u , x ) with graph class Axiom (1), we have that
x : ¬ π B i ( u , x ) ¬ π B t ( u , v , x )
has to be satisfied.
Subpart 2 (transformation specific part of the proof).
For the identity transformation B F ( u , v ) E ( u , v ) holds. With graph class Axiom (3) the expression F ( u , v ) E ( u , v ) w : E ( u , w ) ¬ π B t ( u , w , v ) is derived. Using (A1), (A2) and E(u,w) F ( u , w ) yields the formula in the table (in the following of this proof, the table always refers to Table 3).
Furthermore, with graph class Axiom (4), the expression ¬ F ( u , v ) ¬ E ( u , v ) w : ¬ E ( u , w ) ¬ π B t ( u , v , w ) is derived. Using (A3), (A4) and ¬ E ( u , w ) ¬ F ( u , w ) yields the formula in the table. Note that the existence of F ( u , v ) depends only on E ( u , v ) and for F ( u , v ) and ¬ F ( u , w ) both formulas in the table yield ¬ π B t ( u , w , v ) . Therefore, the expression with the transfer predicate is only written in one of the formulas.
For the B transformation, F ( u , v ) E ( v , u ) holds. With graph class Axiom (3), the expression F ( u , v ) E ( v , u ) w : E ( v , w ) ¬ π B t ( v , w , u ) is derived. Using (A1), (A2) and E ( v , w ) F ( w , v ) yields the formula in the table.
Furthermore, with graph class Axiom (4) the expression ¬ F ( u , v ) ¬ E ( v , u ) w : ¬ E ( v , w ) ¬ π B t ( u , v , w ) is derived. Using (A3), (A4) and ¬ E ( v , w ) ¬ F ( w , v ) yields the formula in the table.
Moreover, for the transformation B , the existence of the F ( u , v ) depends only on one of the edges, in this case E ( v , u ) . Therefore, it is also enough to write the expression with the transfer predicate in only one of the formulas.
For the B + transformation F ( u , v ) E ( u , v ) E ( v , u ) and ¬ F ( u , v ) ¬ E ( u , v ) ¬ E ( v , u ) holds. Furthermore, the transformation is symmetric. Therefore, F ( u , v ) F ( v , u ) resp. ¬ F ( u , v ) ¬ F ( v , u ) has to be included in the formula.
With graph class Axiom (3), the expression F ( u , v ) ( E ( u , v ) x : E ( u , x ) ¬ π B t ( u , x , v ) ) ( E ( v , u ) y : E ( v , y ) ¬ π B t ( v , y , u ) ) is derived. Using (A1), (A2), E ( u , x ) F ( u , x ) and E ( v , y ) F ( v , y ) yields the formula in the table.
Furthermore, with graph class Axiom (4) the expression ¬ F ( u , v ) ( ¬ E ( u , v ) x : ¬ E ( u , x ) ¬ π B t ( u , v , x ) ) ( ¬ E ( v , u ) y : ¬ E ( v , y ) ¬ π B t ( v , u , y ) ) is derived. Using (A3) and (A4) yields the formula in the table. Since the transformation is symmetric, it is enough to list only the condition for ¬ E ( u , v ) in the formula for ¬ F ( u , v ) .
For the B , transformation F ( u , v ) E ( u , v ) E ( v , u ) and ¬ F ( u , v ) ¬ E ( u , v ) ¬ E ( v , u ) holds. Furthermore, the transformation is symmetric. Therefore, F ( u , v ) F ( v , u ) resp. ¬ F ( u , v ) ¬ F ( v , u ) has to be included in the formula.
With graph class Axiom (3) the expression F ( u , v ) ( E ( u , v ) x : E ( u , x ) ¬ π B t ( u , x , v ) ) ( E ( v , u ) y : E ( v , y ) ¬ π B t ( v , y , u ) ) is derived. Using (A1), (A2) yields the formula in the table. Since the transformation is symmetric, it is enough to list only the condition for E ( u , v ) in the formula for F ( u , v ) .
Furthermore, with the graph class Axiom (4), the expression ¬ F ( u , v ) ( ¬ E ( u , v ) x : ¬ E ( u , x ) ¬ π B t ( u , v , x ) ) ( ¬ E ( v , u ) y : ¬ E ( v , y ) ¬ π B t ( v , u , y ) ) is derived. Using (A3), (A4), ¬ E ( u , x ) ¬ F ( u , x ) and ¬ E ( v , y ) ¬ F ( v , y ) yields the formula in the table.
For the B transformation F ( u , v ) E ( u , v ) ¬ E ( v , u ) and ¬ F ( u , v ) ¬ E ( u , v ) E ( v , u ) holds. Furthermore, the transformation is directed. Therefore, F ( u , v ) ¬ F ( v , u ) holds.
With the graph class Axioms (3) and (4) the expression F ( u , v ) ( E ( u , v ) x : E ( u , x ) ¬ π B t ( u , x , v ) ) ( ¬ E ( v , u ) y : ¬ E ( v , y ) ¬ π B t ( v , u , y ) ) is derived. Using (A1)–(A4), E ( u , x ) ¬ F ( x , u ) and ¬ E ( v , y ) ¬ F ( v , y ) yields the formula in the table.
Furthermore, with the graph class Axioms (3) (4), the expression ¬ F ( u , v ) ( ¬ E ( u , v ) x : ¬ E ( u , x ) ¬ π B t ( u , v , x ) ) ( E ( v , u ) y : E ( v , y ) ¬ π B t ( v , y , u ) ) is derived. Using (A1)–(A4), ¬ E ( u , x ) ¬ F ( u , x ) and E ( v , y ) ¬ F ( y , v ) yields the formula in the table.
For the B transformation F ( u , v ) ¬ E ( u , v ) E ( v , u ) and ¬ F ( u , v ) E ( u , v ) ¬ E ( v , u ) holds. Furthermore, the transformation is directed. Therefore, F ( u , v ) ¬ F ( v , u ) holds.
With the graph class Axioms (3) and (4) the expression F ( u , v ) ( ¬ E ( u , v ) x : ¬ E ( u , x ) ¬ π B t ( u , v , x ) ) ( E ( v , u ) y : E ( v , y ) ¬ π B t ( v , y , u ) ) is derived. Using (A1)–(A4), ¬ E ( u , x ) ¬ F ( x , u ) and E ( v , y ) ¬ F ( v , y ) yields the formula in the table.
Furthermore, with the graph class Axioms (3) (4) the expression ¬ F ( u , v ) ( E ( u , v ) x : E ( u , x ) ¬ π B t ( u , x , v ) ) ( ¬ E ( v , u ) y : ¬ E ( v , y ) ¬ π B t ( v , u , y ) ) is derived. Using (A1)–(A4), E ( u , x ) ¬ F ( u , x ) and ¬ E ( v , y ) ¬ F ( y , v ) yields the formula in the table.
For the transformation B no edges can exist, therefore, F ( u , v ) and ¬ F ( u , v ) hold.
The formulas for the negated transformations can be obtained by switching the formulas for F ( u , v ) and ¬ F ( u , v ) and also switching F ( u , v ) and ¬ F ( u , v ) for any pair of vertices inside the formula.
Part 2 (⇐).
Assume now that we have a graph H = ( V , F ) such that the edge inclusion and exclusion implications depicted for B γ in Table 3 are satisfied. We construct a graph G = ( V , E ) such that G B and G γ = H , which then implies H B γ .
Construction of G = ( V , E ) is conducted in two steps, a preprocessing and a postprocessing step. The preprocessing is the same for all graph class transformations, while for the postprocssing the specific conditions for the graph classes have to be considered. We begin with a configuration, where all E ( u , v ) are set to true . First, we keep those E ( u , v ) to true resp. set those E ( u , v ) to false , which are enforced or forbidden due to the graph class axioms of class B . We then set the remaining edges E ( u , v ) , which have not been determined in preprocessing accordingly, such that G still satisfies B and at the same time satisfies G γ = H .
Preprocessing (forbidden edges): In order to satisfy graph class Axiom (2), for all u , v V , which satisfy π B e ( u , v ) , we set E ( u , v ) to false ; in this case, in order to also satisfy the Axiom (3), we set E ( u , y ) to false for all y V for which π B t ( u , v , y ) is satisfied.
Preprocessing (enforced edges): In order to satisfy graph class Axiom (1), for all u , v V which satisfy π B i ( u , v ) , we set E ( u , v ) to true ; in this case, in order to satisfy also Axiom (3), we set E ( u , x ) to true for all x V for which π B t ( u , x , v ) is satisfied. Soundness of inclusion, exclusion and transfer predicates assures that we do not set any E ( u , v ) and E ( u , y ) to true , which we have set to false before.
Postprocessing: Now, we consider the implications for the specific transformations.
For the identity transformation B F ( u , v ) ¬ π B e ( u , v ) holds; therefore, the edge E ( u , v ) was not set to false in the preprocesing and can be set to true now.
Furthermore, ¬ F ( u , v ) ¬ π B i ( u , v ) w : ¬ F ( u , w ) ¬ π B t ( u , v , w ) assures that E ( u , v ) was not set to true in the preprocessing and is also not enforced by the existence of another edge E ( u , w ) , since F ( u , w ) E ( u , w ) .
For B , F ( u , v ) ¬ π B e ( v , u ) holds; therefore, the edge E ( v , u ) was not set to false in the preprocessing and can be set to true now.
Furthermore, ¬ F ( u , v ) ¬ π B i ( v , u ) w : ¬ F ( w , v ) ¬ π B t ( v , u , w ) assures that E ( v , u ) was not set to true in the preprocessing and is also not enforced by the existence of another edge E ( v , w ) , since F ( w , v ) E ( v , w ) .
For the transformation B + we start with the implication for ¬ F ( u , v ) , because E ( u , v ) and E ( v , u ) have to be set to false for ¬ F ( u , v ) . The implication for ¬ F ( u , v ) ¬ F ( v , u ) ¬ π B i ( u , v ) w : ¬ π B i ( u , w ) ¬ π B t ( u , v , w ) assures that E ( u , v ) was not set to true in the prepossessing and is also enforced by the existence of other edges. Therefore, we can set E ( u , v ) to false now. The symmetry of F ( u , v ) assures that the same holds for E ( v , u ) ; therefore, we can also set E ( v , u ) to false now.
Now, consider the implication for F ( u , v ) and assume first that F ( u , v ) ( ¬ π B e ( u , v ) x : F ( u , x ) ¬ π B e ( u , x ) ¬ π B t ( u , x , v ) ) holds. This implication assures that E ( u , v ) was not set to false in the preprocessing. Furthermore, E ( u , v ) can also not be set to false , by the non-existence of an other edge, because if π B t ( u , x , v ) holds, then also F ( u , x ) holds and therefore E ( u , x ) can be set to true , too. Therefore, E ( u , v ) can be set to true now. With the same argument, E ( v , u ) can be set to true if F ( u , v ) ( ¬ π B e ( v , u ) y : F ( u , y ) ¬ π B e ( u , y ) ¬ π B t ( v , y , u ) ) holds.
For the transformation B , we start with the implication for F ( u , v ) , because E ( u , v ) and E ( v , u ) have to be set to true for F ( u , v ) . The implication F ( u , v ) ¬ π B e ( u , v ) w : ¬ π B e ( u , w ) ¬ π B t ( u , w , v ) assures that E ( u , v ) was not set to false in the preprocessing and is also not removed by the non-existence of other edges. Therefore, we can set E ( u , v ) to true now.The symmetry of F ( u , v ) assures that the same holds for E ( v , u ) ; therefore, we can also set E ( v , u ) to true now.
Now, consider the implication for ¬ F ( u , v ) and assume first that ¬ F ( u , v ) ( ¬ π B i ( u , v ) x : ¬ F ( u , x ) ¬ π B i ( u , x ) ¬ π B t ( u , v , x ) ) holds. This implication assures that E ( u , v ) was not set to true in the preprocessing. Furthermore, E ( u , v ) can also not be set to true , by the existence of any other edge, because if π B t ( u , v , x ) holds, then also ¬ F ( u , x ) holds and therefore E ( u , x ) can be set to false , too. Therefore, E ( u , v ) can be set to true now. With the same argument E ( v , u ) can be set to false if ¬ F ( u , v ) ( ¬ π B i ( v , u ) y : ¬ F ( v , y ) ¬ π B i ( v , y ) ¬ π B t ( v , u , y ) ) holds.
For the transformation B , we start with the implication for F ( u , v ) , because E ( u , v ) has to be set to true and E ( v , u ) has to be set to false for F ( u , v ) . We consider first the first part of the implication that assures that E ( u , v ) can be set to true and afterwards the second part of the implication that assures that E ( v , u ) can be set to false . The implication F ( u , v ) ¬ π B e ( u , v ) x : ( ¬ π B e ( u , x ) ¬ F ( x , u ) ) ¬ π B t ( u , x , v ) assures that E ( u , v ) was not set to false in the preprocessing.Furthermore, E ( u , v ) can also not be set to false , by the existence of an other edge, because if π B t ( u , x , v ) holds, then also ¬ F ( x , u ) holds and therefore E ( u , x ) can be set to true as well. Therefore, we can set E ( u , v ) to true now.
The implication F ( u , v ) π B i ( v , u ) y : ( ¬ π B i ( v , y ) ¬ F ( v , y ) ) ¬ π B t ( v , u , y ) assures that E ( v , u ) was not set to true in the prepossessing. Furthermore, E ( v , u ) can as well not be set to false , by the existence of another edge, because if π B t ( v , u , y ) holds, then also ¬ F ( v , y ) holds and therefore E ( v , y ) can be set to false as well. Therefore, we can set E ( v , u ) to false now.
With the same argumentation, the implication for ¬ F ( u , v ) assures that E ( u , v ) can be set to false or E ( v , u ) can be set to true , if ¬ F ( u , v ) holds.
For the transformation B , we start with the implication for F ( u , v ) , because E ( u , v ) has to be set to false and E ( v , u ) has to be set to true for F ( u , v ) . We consider first the first part of the implication that assures that E ( v , u ) can be set to true and afterwards the second part of the implication that assures that E ( u , v ) can be set to false . The implication F ( u , v ) ¬ π B e ( v , u ) y : ( ¬ π B e ( v , y ) ¬ F ( v , y ) ) ¬ π B t ( v , y , u ) assures that E ( v , u ) was not set to false in the preprocessing. Furthermore, E ( v , u ) can also not be set to false , by the existence of an other edge, because if π B t ( v , y , u ) holds, then also ¬ F ( v , y ) holds and therefore E ( v , y ) can be set to true as well. Therefore, we can set E ( v , u ) to true now.
The implication F ( u , v ) π B i ( u , v ) x : ( ¬ π B i ( u , x ) ¬ F ( x , u ) ) ¬ π B t ( u , v , x ) assures that E ( u , v ) was not set to true in the prepossessing. Furthermore, E ( u , v ) can also be not set to false , by the existence of an other edge, because if π B t ( u , v , x ) holds, then also ¬ F ( x , u ) holds and therefore E ( u , x ) can be set to false as well. Therefore, we can set E ( u , v ) to false now.
With the same argumentation, the implication for ¬ F ( u , v ) assures that E ( u , v ) can be set to true or E ( v , u ) can be set to false if ¬ F ( u , v ) holds.
For the transformation B , no transformation specific restrictions have to be considered, because every graph is transformed to the empty graph. Therefore, after the preprocessing, the remaining edges can be set to true or false arbitrarily.
The proofs for the negated transformations can be obtained analogously. □

References

  1. Frey, H.; Böltz, L. Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion and Transfer Axioms. In Proceedings of the 33rd Canadian Conference on Computational Geometry, CCCG 2021, Halifax, NS, Canada, 10–12 August 2021; pp. 127–138. [Google Scholar]
  2. Gabbay, D.M.; Schmidt, R.A.; Szalas, A. Studies in logic: Mathematical logic and foundations. In Second-Order Quantifier Elimination—Foundations, Computational Aspects and Applications; College Publications: Rickmansworth, UK, 2008; Volume 12. [Google Scholar]
  3. Bachmair, L.; Ganzinger, H.; Waldmann, U. Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 1994, 5, 193–212. [Google Scholar] [CrossRef]
  4. Barrière, L.; Fraigniaud, P.; Narayanan, L.; Opatrny, J. Robust position-based routing in wireless ad hoc networks with irregular transmission ranges. Wirel. Commun. Mob. Comput. 2003, 3, 141–153. [Google Scholar] [CrossRef]
  5. Kuhn, F.; Wattenhofer, R.; Zollinger, A. Ad hoc networks beyond unit disk graphs. Wirel. Netw. 2008, 14, 715–729. [Google Scholar] [CrossRef]
  6. Blough, D.M.D.; Leoncini, M.; Resta, G.; Santi, P. The k-Neighbors Approach to Interference Bounded and Symmetric Topology Control in Ad Hoc Networks. IEEE Trans. Mob. Comput. 2006, 5, 1267–1282. [Google Scholar] [CrossRef]
  7. von Rickenbach, P.; Wattenhofer, R.; Zollinger, A. Algorithmic Models of Interference in Wireless Ad Hoc and Sensor Networks. IEEE/ACM Trans. Netw. 2009, 17, 172–185. [Google Scholar] [CrossRef]
  8. Peleg, D.; Roditty, L. Localized spanner construction for Ad Hoc networks with variable transmission range. ACM Trans. Sens. Netw. 2010, 7, 25:1–25:14. [Google Scholar] [CrossRef] [Green Version]
  9. Moaveninejad, K.; Song, W.Z.; Li, X.Y. Robust position-based routing for wireless ad hoc networks. Ad Hoc Netw. 2005, 3, 546–559. [Google Scholar] [CrossRef]
Figure 1. Illustration of the used notation. Solid blue line: u v G , dashed blue line: u v G , solid green line: u v H , dashed green line: u v H , solid red line: π B i ( u , v ) , dashed red line π B e ( u , v ) , and red link from u w to u v : π B t ( u , v , w ) holds.
Figure 1. Illustration of the used notation. Solid blue line: u v G , dashed blue line: u v G , solid green line: u v H , dashed green line: u v H , solid red line: π B i ( u , v ) , dashed red line π B e ( u , v ) , and red link from u w to u v : π B t ( u , v , w ) holds.
Information 13 00578 g001
Figure 2. Counterexamples for including and excluding a single edge u v .
Figure 2. Counterexamples for including and excluding a single edge u v .
Information 13 00578 g002
Figure 3. Counterexamples for including and excluding more than one edge.
Figure 3. Counterexamples for including and excluding more than one edge.
Information 13 00578 g003
Figure 4. The relations of the base graph classes.
Figure 4. The relations of the base graph classes.
Information 13 00578 g004
Table 1. The eight non-negated vertex preserving simple graph transformations.
Table 1. The eight non-negated vertex preserving simple graph transformations.
δ ( E ( u , v ) , E ( v , u ) )
E ( u , v ) 0011
NameSymbol E ( v , u ) 0101Symmetry
Symmetric subgraph G F ( u , v ) 0001Symmetric
Symmetric supergraph G + F ( u , v ) 0111Symmetric
xor graph G F ( u , v ) 0110Symmetric
Empty graph G F ( u , v ) 0000Symmetric
Identity graph G id F ( u , v ) 0011
Reversed graph G F ( u , v ) 0101
Outgoing directed subgraph G F ( u , v ) 0010Directed
Incoming directed subgraph G F ( u , v ) 0100Directed
Table 2. The eight negated vertex preserving simple graph transformations.
Table 2. The eight negated vertex preserving simple graph transformations.
δ ( E ( u , v ) , E ( v , u ) )
E ( u , v ) 0011
Symbol E ( v , u ) 0101Symmetry
G ¬ F ( u , v ) 1110Symmetric
G ¬ + F ( u , v ) 1000Symmetric
G ¬ F ( u , v ) 1001Symmetric
G ¬ F ( u , v ) 1111Symmetric
G ¬ id F ( u , v ) 1100
G ¬ F ( u , v ) 1010
G ¬ F ( u , v ) 1101Complementary directed
G ¬ F ( u , v ) 1011Complementary directed
Table 3. The expressions implied by edge existence and non-existence under the considered vertex preserve the simple graph class transformations in Γ . Quantification is over all vertices V of the considered graph H = ( V , F ) . The maximum size of a minimum witness graph to find a counter example is expressed by μ ( γ ) .
Table 3. The expressions implied by edge existence and non-existence under the considered vertex preserve the simple graph class transformations in Γ . Quantification is over all vertices V of the considered graph H = ( V , F ) . The maximum size of a minimum witness graph to find a counter example is expressed by μ ( γ ) .
γ Edge Inclusion and Exclusion Implications μ ( γ )
H B F ( u , v ) 1
¬ F ( u , v )
H B ¬ F ( u , v ) 1
¬ F ( u , v )
H B F ( u , v ) ¬ π B e ( u , v ) 3
¬ F ( u , v ) ¬ π B i ( u , v ) w : ¬ F ( u , w ) ¬ π B t ( u , v , w )
H B ¬ F ( u , v ) ¬ π B i ( u , v ) 3
¬ F ( u , v ) ¬ π B e ( u , v ) w : ¬ F ( u , w ) ¬ π B t ( u , w , v )
H B F ( u , v ) F ( v , u ) ¬ π B e ( u , v ) w : ¬ π B e ( u , w ) ¬ π B t ( u , w , v ) 4
¬ F ( u , v ) ( ¬ π B i ( u , v ) x : ¬ F ( u , x ) ¬ π B i ( u , x ) ¬ π B t ( u , v , x ) )
( ¬ π B i ( v , u ) y : ¬ F ( v , y ) ¬ π B i ( v , y ) ¬ π B t ( v , u , y ) )
H B ¬ F ( u , v ) ( ¬ π B i ( u , v ) x : F ( u , x ) ¬ π B i ( u , x ) ¬ π B t ( u , v , x ) ) 4
( ¬ π B i ( v , u ) y : F ( v , y ) ¬ π B i ( v , y ) ¬ π B t ( v , u , y ) )
¬ F ( u , v ) ¬ F ( v , u ) ¬ π B e ( u , v ) w : ¬ π B e ( u , w ) ¬ π B t ( u , w , v )
H B + F ( u , v ) ( ¬ π B e ( u , v ) x : F ( u , x ) ¬ π B e ( u , x ) ¬ π B t ( u , x , v ) ) 4
( ¬ π B e ( v , u ) y : F ( v , y ) ¬ π B e ( v , y ) ¬ π B t ( v , y , u ) )
¬ F ( u , v ) ¬ F ( v , u ) ¬ π B i ( u , v ) w : ¬ π B i ( u , w ) ¬ π B t ( u , v , w )
H B ¬ + F ( u , v ) F ( v , u ) ¬ π B i ( u , v ) w : ¬ π B i ( u , w ) ¬ π B t ( u , v , w ) 4
¬ F ( u , v ) ( ¬ π B e ( u , v ) x : ¬ F ( u , x ) ¬ π B e ( u , x ) ¬ π B t ( u , x , v ) )
( ¬ π B e ( v , u ) y : ¬ F ( v , y ) ¬ π B e ( v , y ) ¬ π B t ( v , y , u ) )
H B F ( u , v ) ¬ π B e ( v , u ) 3
¬ F ( u , v ) ¬ π B i ( v , u ) w : ¬ F ( w , v ) ¬ π B t ( v , u , w )
H B ¬ F ( u , v ) ¬ π B i ( v , u ) w : F ( w , v ) ¬ π B t ( v , u , w ) 3
¬ F ( u , v ) ¬ π B e ( v , u )
H B F ( u , v ) ¬ F ( v , u ) ¬ π B e ( u , v ) x : ( ¬ π B e ( u , x ) ¬ F ( x , u ) ) ¬ π B t ( u , x , v ) 4
¬ π B i ( v , u ) y : ( ¬ π B i ( v , y ) ¬ F ( v , y ) ) ¬ π B t ( v , u , y )
¬ F ( u , v ) ¬ π B i ( u , v ) x : ( ¬ π B i ( u , x ) ¬ F ( u , x ) ) ¬ π B t ( u , v , x )
¬ π B e ( v , u ) y : ( ¬ π B e ( v , y ) ¬ F ( y , v ) ) ¬ π B t ( v , y , u )
H B ¬ F ( u , v ) ¬ π B i ( u , v ) x : ( ¬ π B i ( u , x ) F ( u , x ) ) ¬ π B t ( u , v , x ) 4
¬ π B e ( v , u ) y : ( ¬ π B e ( v , y ) F ( y , v ) ) ¬ π B t ( v , y , u )
¬ F ( u , v ) F ( v , u ) ¬ π B e ( u , v ) x : ( ¬ π B e ( u , x ) F ( x , u ) ) ¬ π B t ( u , x , v )
¬ π B i ( v , u ) y : ( ¬ π B i ( v , y ) F ( v , y ) ) ¬ π B t ( v , u , y )
H B F ( u , v ) ¬ F ( v , u ) ¬ π B e ( v , u ) y : ( ¬ π B e ( v , y ) ¬ F ( v , y ) ) ¬ π B t ( v , y , u ) 4
¬ π B i ( u , v ) x : ( ¬ π B i ( u , x ) ¬ F ( x , u ) ) ¬ π B t ( u , v , x )
¬ F ( u , v ) ¬ π B i ( v , u ) y : ( ¬ π B i ( v , y ) ¬ F ( y , v ) ) ¬ π B t ( v , u , y )
¬ π B e ( u , v ) x : ( ¬ π B e ( u , x ) ¬ F ( u , x ) ) ¬ π B t ( u , x , v )
H B ¬ F ( u , v ) ¬ π B i ( v , u ) y : ( ¬ π B i ( v , y ) F ( y , v ) ) ¬ π B t ( v , u , y ) 4
¬ π B e ( u , v ) x : ( ¬ π B e ( u , x ) F ( u , x ) ) ¬ π B t ( u , x , v )
¬ F ( u , v ) F ( v , u ) ¬ π B e ( v , u ) y : ( ¬ π B e ( v , y ) F ( v , y ) ) ¬ π B t ( v , y , u )
¬ π B i ( u , v ) x : ( ¬ π B i ( u , x ) ¬ F ( x , u ) ) ¬ π B t ( u , v , x )
Table 4. The expressions to be combined line-by-line as the nonnegated form on the left side and negated form on the right side to test for subclass relations.
Table 4. The expressions to be combined line-by-line as the nonnegated form on the left side and negated form on the right side to test for subclass relations.
γ Edge Inclusion and Exclusion Implications
( · ) ρ B 1 ( { u v } , { } , V ) = true
ρ B 2 ( { } , { u v } , V ) = false
( · ) id ρ B 1 ( { u v } , { } , V ) = π B e ( u , v )
ρ B 2 ( { } , { u v } , V ) = π B i ( u , v )
ρ B 3 ( { u v , v u } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v u } , { } , V )
ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 5 ( { u v } , { v u } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V ) π B t ( u , w , v ) v = w
ρ B 7 ( { v u } , { w u } , V ) = ρ B 1 ( { v u } , { } , V ) ρ B 2 ( { } , { w u } , V ) v = w
ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V )
ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V )
ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V ) u = w v = x
ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
( · ) + ρ B + 1 ( { u v } , { } , V ) = π B e ( u , v ) π B e ( v , u )
ρ B + 2 ( { } , { u v } , V ) = π B i ( u , v ) π B i ( v , u )
ρ B + 3 ( { u v , v u } , { } , V ) = ρ B + 1 ( { u v } , { } , V )
ρ B + 4 ( { } , { u v , v u } , V ) = ρ B + 2 ( { } , { u v } , V )
ρ B + 5 ( { u v } , { v u } , V ) = true
ρ B + 6 ( { u v } , { u w } , V ) = ρ B + 1 ( { u v } , { } , V ) ρ B + 2 ( { } , { u w } , V )
( π B t ( u , w , v ) π B e ( v , u ) ) v = w
ρ B + 7 ( { v u } , { w u } , V ) = ρ B + 6 ( { u v } , { u w } , V )
ρ B + 8 ( { u v , v w } , { } , V ) = ρ B + 1 ( { u v } , { } , V ) ρ B + 1 ( { v w } , { } , V )
ρ B + 9 ( { } , { u v , v w } , V ) = ρ B + 2 ( { } , { u v } , V ) ρ B + 2 ( { } , { v w } , V )
ρ B + 10 ( { u v , w x } , { w v } , V ) = ρ B + 7 ( { u v } , { w v } , V ) ρ B + 6 ( { w x } , { w v } , V ) u = w v = x
ρ B + 11 ( { w v } , { u v , w x } , V ) = ρ B + 7 ( { w v } , { u v } , V ) ρ B + 6 ( { w v } , { w x } , V )
( π B t ( v , u , w ) π B t ( w , x , v ) ) u = w v = x
( · ) ρ B 1 ( { u v } , { } , V ) = π B e ( u , v ) π B e ( v , u )
ρ B 2 ( { } , { u v } , V ) = π B i ( u , v ) π B i ( v , u )
ρ B 3 ( { u v , v u } , { } , V ) = ρ B 1 ( { u v } , { } , V )
ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V )
ρ B 5 ( { u v } , { v u } , V ) = true
ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V )
( π B t ( u , w , v ) π B i ( w , u ) ) v = w
ρ B 7 ( { v u } , { w u } , V ) = ρ B 6 ( { u v } , { u w } , V )
ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V )
ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V )
ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V )
( π B t ( v , w , u ) π B t ( w , v , x ) ) u = w v = x
ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
Table 5. The expressions to be combined line-by-line as a nonnegated form on the left side and negated form on the right side to test for subclass relations.
Table 5. The expressions to be combined line-by-line as a nonnegated form on the left side and negated form on the right side to test for subclass relations.
γ Edge Inclusion and Exclusion Implications
( · ) ρ B 1 ( { u v } , { } , V ) = π B e ( v , u )
ρ B 2 ( { } , { u v } , V ) = π B i ( v , u )
ρ B 3 ( { u v , v u } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v u } , { } , V )
ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 5 ( { u v } , { v u } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V ) v = w
ρ B 7 ( { v u } , { w u } , V ) = ρ B 1 ( { v u } , { } , V ) ρ B 2 ( { } , { w u } , V ) π B t ( u , w , v ) v = w
ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V )
ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V )
ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V ) u = w v = x
ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
( · ) ρ B 1 ( { u v } , { } , V ) = π B e ( u , v ) π B i ( v , u )
ρ B 2 ( { } , { u v } , V ) = π B i ( u , v ) π B e ( v , u )
ρ B 3 ( { u v , v u } , { } , V ) = true
ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 5 ( { u v } , { v u } , V ) = ρ B 1 ( { u v } , { } , V )
ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V )
( π B t ( u , w , v ) π B e ( w , u ) ) v = w
ρ B 7 ( { v u } , { w u } , V ) = ρ B 1 ( { v u } , { } , V ) ρ B 2 ( { } , { w u } , V )
( π B t ( u , v , w ) π B i ( w , u ) ) v = w
ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V ) π B t ( v , u , w ) u = w
ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V )
π B i ( u , v ) π B e ( w , v ) π B t ( v , w , u )
ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V )
( π B t ( v , u , w ) π B t ( w , v , x ) ) u = w v = x
ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
( · ) ρ B 1 ( { u v } , { } , V ) = π B i ( u , v ) π B e ( v , u )
ρ B 2 ( { } , { u v } , V ) = π B e ( u , v ) π B i ( v , u )
ρ B 3 ( { u v , v u } , { } , V ) = true
ρ B 4 ( { } , { u v , v u } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v u } , V )
ρ B 5 ( { u v } , { v u } , V ) = ρ B 1 ( { u v } , { } , V )
ρ B 6 ( { u v } , { u w } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 2 ( { } , { u w } , V )
( π B t ( u , v , w ) π B i ( u , w ) ) v = w
ρ B 7 ( { v u } , { w u } , V ) = ρ B 1 ( { v u } , { } , V ) ρ B 2 ( { } , { w u } , V )
( π B t ( u , w , v ) π B e ( w , u ) ) v = w
ρ B 8 ( { u v , v w } , { } , V ) = ρ B 1 ( { u v } , { } , V ) ρ B 1 ( { v w } , { } , V ) π B t ( v , w , u ) u = w
ρ B 9 ( { } , { u v , v w } , V ) = ρ B 2 ( { } , { u v } , V ) ρ B 2 ( { } , { v w } , V )
π B e ( u , v ) π B i ( w , v ) π B t ( v , u , w )
ρ B 10 ( { u v , w x } , { w v } , V ) = ρ B 7 ( { u v } , { w v } , V ) ρ B 6 ( { w x } , { w v } , V )
( π B t ( v , w , u ) π B t ( w , x , v ) ) u = w v = x
ρ B 11 ( { w v } , { u v , w x } , V ) = ρ B 7 ( { w v } , { u v } , V ) ρ B 6 ( { w v } , { w x } , V ) u = w v = x
Publisher’s Note: MDPI stays neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Share and Cite

MDPI and ACS Style

Böltz, L.; Frey, H. Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion, and Transfer Axioms under Simple Transformations. Information 2022, 13, 578. https://doi.org/10.3390/info13120578

AMA Style

Böltz L, Frey H. Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion, and Transfer Axioms under Simple Transformations. Information. 2022; 13(12):578. https://doi.org/10.3390/info13120578

Chicago/Turabian Style

Böltz, Lucas, and Hannes Frey. 2022. "Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion, and Transfer Axioms under Simple Transformations" Information 13, no. 12: 578. https://doi.org/10.3390/info13120578

APA Style

Böltz, L., & Frey, H. (2022). Automatically Testing Containedness between Geometric Graph Classes defined by Inclusion, Exclusion, and Transfer Axioms under Simple Transformations. Information, 13(12), 578. https://doi.org/10.3390/info13120578

Note that from the first issue of 2016, this journal uses article numbers instead of page numbers. See further details here.

Article Metrics

Back to TopTop