sub graph (subGraph)

The relation between two Graphs when one Graph is a part of the other. (subGraph graph1 graph2) means that graph1 is a part of graph2.

Ontology

SUMO / GRAPH-THEORY

Class(es)

class

inheritable relation

binary predicate
is instance of

reflexive relation
is instance of

transitive relation
is instance of

sub graph

Coordinate term(s)

arc weight authors before before or equal causes causes subclass citizen closed on connected contains information cooccur copy crosses date decreases likelihood developmental form disjoint distributes documentation duration during earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element in list in scope of interest increases likelihood independent probability inhabits inhibits initial list instance interior part inverse irreflexive on larger less than less than or equal to material measure meets temporally modal attribute overlaps spatially overlaps temporally parent partial ordering on partly located path length possesses precondition prevents proper part property publishes range range subclass refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub list sub organizations sub plan sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure superficial part temporal part time total ordering on trichotomizing on uses valence version

Type restrictions

subGraph(graph, graph)

Axioms (3)

If graph is an instance of graph and node1 is an instance of graph node and node2 is an instance of graph node and node1 is a part of graph and node2 is a part of graph and node1 is not equal to node2, then there exist arc,path so that

arc links node1 and node2
- path is a subgraph of graph
- path is an instance of graph path
- - "the beginning of path" is equal to node1 and "the end of path" is equal to node2
  - "the beginning of path" is equal to node2 and "the end of path" is equal to node1

(=>
      (and
            (instance ?GRAPH Graph)
            (instance ?NODE1 GraphNode)
            (instance ?NODE2 GraphNode)
            (graphPart ?NODE1 ?GRAPH)
            (graphPart ?NODE2 ?GRAPH)
            (not
                  (equal ?NODE1 ?NODE2)))
      (exists
            (?ARC ?PATH)
            (or
                  (links ?NODE1 ?NODE2 ?ARC)
                  (and
                        (subGraph ?PATH ?GRAPH)
                        (instance ?PATH GraphPath)
                        (or
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE1)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE2))
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE2)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE1)))))))

If graph1 is a subgraph of graph2 and element is a part of graph1, then element is a part of graph2.

(=>
      (and
            (subGraph ?GRAPH1 ?GRAPH2)
            (graphPart ?ELEMENT ?GRAPH1))
      (graphPart ?ELEMENT ?GRAPH2))

if
- "the value of path" is equal to sum
- subpath is a subgraph of path
- arc1 is a part of path
- the value of arc1 is number1
- for all arc2 holds: if arc2 is a part of path, then arc2 is a part of subpath or arc2 is equal to arc1
,
then sum is equal to "("the value of subpath"+number1)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))