graph part (graphPart)

A basic relation for Graphs and their parts. (graphPart part graph) means that part is a GraphArc or GraphNode of the Graph graph.

Ontologie

SUMO / GRAPH-THEORY

Class(es)

třída

inheritable relation

binární predikát
is instance of

nesymetrická relace
is instance of

ireflexivní relace
is instance of

graph part

Související termín(y)

back fn cardinality fn front fn principal host fn probability fn skin fn arc weight attribute authors before before or equal causes causes subclass citizen closed on completely fills connected connected engineering components 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 fills finishes frequency greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element immediate instance immediate subclass 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 manner material measure meets spatially meets temporally member modal attribute overlaps partially overlaps temporally parent partial ordering on partially fills partly located path length penetrates possesses precondition prevents proper part properly fills property publishes range range subclass realization refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph 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 surface temporal part time total ordering on trichotomizing on uses valence version

Typy argumentů

graphPart(prvek grafu, graf)

Axiomy (13)

Jestliže graph je instancí třídy graf a node1 je instancí třídy uzel grafu a node2 je instancí třídy uzel grafu a node1 je částí graph a node2 je částí graph a node1 se nerovná node2, potom existují arc,path tak, že

arc spojuje node1 a node2
- path je podgrafem graph
- path je instancí třídy cesta v grafu
- - "the beginning of path" se rovná node1 a "the end of path" se rovná node2
  - "the beginning of path" se rovná node2 a "the end of path" se rovná 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)))))))

Jestliže graph je instancí třídy graf, potom existují node1,node2,node3,arc1,arc2 tak, že node1 je částí graph a node2 je částí graph a node3 je částí graph a arc1 je částí graph a arc2 je částí graph a node2 spojuje arc1 a node1 a node3 spojuje arc2 a node2 a node1 se nerovná node2 a node2 se nerovná node3 a node1 se nerovná node3 a arc1 se nerovná arc2.

(=>
      (instance ?GRAPH Graph)
      (exists
            (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
            (and
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (graphPart ?NODE3 ?GRAPH)
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (links ?ARC1 ?NODE1 ?NODE2)
                  (links ?ARC2 ?NODE2 ?NODE3)
                  (not
                        (equal ?NODE1 ?NODE2))
                  (not
                        (equal ?NODE2 ?NODE3))
                  (not
                        (equal ?NODE1 ?NODE3))
                  (not
                        (equal ?ARC1 ?ARC2)))))

Jestliže graph je instancí třídy orientovaný graf a arc je instancí třídy hrana grafu a arc je částí graph, potom existují node1,node2 tak, že "initial node fn(arc)" se rovná node1 a "terminal node fn(arc)" se rovná node2.

(=>
      (and
            (instance ?GRAPH DirectedGraph)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (exists
            (?NODE1 ?NODE2)
            (and
                  (equal
                        (InitialNodeFn ?ARC)
                        ?NODE1)
                  (equal
                        (TerminalNodeFn ?ARC)
                        ?NODE2))))

Jestliže graph je instancí třídy strom, potom neexistuje smyčka grafu loop tak, že loop je částí graph.

(=>
      (instance ?GRAPH Tree)
      (not
            (exists
                  (?LOOP)
                  (and
                        (instance ?LOOP GraphLoop)
                        (graphPart ?LOOP ?GRAPH)))))

jestliže graph je instancí třídy cesta v grafu a arc je instancí třídy hrana grafu a arc je částí graph,
potom jestliže "initial node fn(arc)" se rovná node, potom neexistuje other tak, že "initial node fn(other)" se rovná node a other se nerovná arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (InitialNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

jestliže graph je instancí třídy cesta v grafu a arc je instancí třídy hrana grafu a arc je částí graph,
potom jestliže "terminal node fn(arc)" se rovná node, potom neexistuje other tak, že "terminal node fn(other)" se rovná node a other se nerovná arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (TerminalNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

graph je instancí třídy multigraf tehdy a jen tehdy pokud existují arc1,arc2,node1,node2 tak, že arc1 je částí graph a arc2 je částí graph a node1 je částí graph a node2 je částí graph a arc1 spojuje node1 a node2 a arc2 spojuje node1 a node2 a arc1 se nerovná arc2.

(<=>
      (instance ?GRAPH MultiGraph)
      (exists
            (?ARC1 ?ARC2 ?NODE1 ?NODE2)
            (and
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (links ?NODE1 ?NODE2 ?ARC1)
                  (links ?NODE1 ?NODE2 ?ARC2)
                  (not
                        (equal ?ARC1 ?ARC2)))))

graph je instancí třídy pseudograf tehdy a jen tehdy pokud existuje smyčka grafu loop tak, že loop je částí graph.

(<=>
      (instance ?GRAPH PseudoGraph)
      (exists
            (?LOOP)
            (and
                  (instance ?LOOP GraphLoop)
                  (graphPart ?LOOP ?GRAPH))))

Jestliže part je instancí třídy prvek grafu, potom existuje graf graph tak, že part je částí graph.

(=>
      (instance ?PART GraphElement)
      (exists
            (?GRAPH)
            (and
                  (instance ?GRAPH Graph)
                  (graphPart ?PART ?GRAPH))))

Jestliže graph1 je podgrafem graph2 a element je částí graph1, potom element je částí graph2.

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

jestliže
- "path weight fn(path)" se rovná sum
- subpath je podgrafem path
- arc1 je částí path
- arc weight(arc1,number1) platí
- pro všechny arc2 platí: jestliže arc2 je částí path, potom arc2 je částí subpath nebo arc2 se rovná arc1
,
potom sum se rovná "("path weight fn(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)))

jestliže
- "path weight fn(path)" se rovná sum
- arc1 je částí path
- arc2 je částí path
- arc weight(arc1,number1) platí
- arc weight(arc2,number2) platí
- pro všechny arc3 platí: jestliže arc3 je částí path, potom arc3 se rovná arc1 nebo arc3 se rovná arc2
,
potom "path weight fn(path)" se rovná "(number1+number2)"

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

Jestliže path je částí graph a graph není instancí třídy orientovaný graf, potom "graph path fn(node1,node2)" se rovná path tehdy a jen tehdy pokud "graph path fn(node2,node1)" se rovná path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))