graphenTeil (graphPart)

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

Ontology

SUMO / GRAPH-THEORY

Class(es)

Kategorie

inheritable relation

zweistellige Prädikat
is instance of

asymmetrische Relation
is instance of

irreflexive Relation
is instance of

graphenTeil

Coordinate term(s)

RückseiteFn KardinalitätFn FrontseiteFn HauptwirtFn Wahrscheinlichkeit OberflächeFn arctusGewicht attribut schreibt vor vorOderGleichzeitig verursacht causes subclass bürger aufgeschlossen fülltVollständig angeschlossen angeschlosseneTechnikKomponenten enthältInformationen zusammenGeschiecht kopie kreuzt datum verringertWahrscheinlichkeit entwicklungsForm disjunkt istDistributiv dokumentation &%dauer von %1 ist %2 %n{nicht} während früh herausgeber element beschäftigt %1 ist gleich %2 %n{nicht} äquivalenzrelationMit nutztAus inSpracheAusgedrückt stelltGegenüber verwandt füllt beendet frequenz grösserAls grösserAlsOderGleich hatZweck hatFähigkeit hältWährend hatVerpflichtung hatRecht loch identitätsElement direkterFall direckteTeilkategorie inListe imBereichInteresses vergrössertWahrscheinlichkeit Unabhänigkeitswahrscheinlichkeit wohnt hemmt ausgangsList fall innenteil umkehrFunktion irreflexivAur grösser kleinerAls kleinerAlsOderGleich weise material mass schliesstRäumlichAn schliesstZeitlichAn mitglied modalesAttribute decktSichTeilweise decktSichZeitlich elternteil teilweiseEinrichtung fülltTeilweise befindetSichTeils pfadLänge dringtEin besitzt vorbedingung verhindert korrektesTeil fülltRichtig eigenschaft veröffentlicht &%bildbereich von %1 ist ein fall von %2 {nicht} bildbereichTeilkategorie realizierung beziehtSichAuf reflexivAuf verwandtesInnenkonzept geschwister kleiner beginnt teilAttribut teilsammlung teilGraph teilliste unterOrganisation teilplan subProzess %1 ist eine &%teilangelegenheit von %2 %n{nicht} teilkategorie teilrelation fasstInhaltsKategorieZusammen fasstInhaltsFallZusammen nachfolgerAttribut nachfolgerAttributSchliessung oberflächichesTeil fläche zeitlichesTeil zeit gesamteinrichtung trichotomizierungAuf verwendet valenz version

Type restrictions

graphPart(Graphelement, Graph)

Axioms (13)

Wenn graph ist ein fall von Graph und node1 ist ein fall von Graphknoten und node2 ist ein fall von Graphknoten und node1 ist ein teil von graph und node2 ist ein teil von graph und node1 ist gleich node2 nicht, dann es gibt ein arc,path der

arc verbindet node1 und node2
- path ist ein teilgraph von graph
- path ist ein fall von Graphweg
- - "der anfang von path" ist gleich node1 und "das ende von path" ist gleich node2
  - "der anfang von path" ist gleich node2 und "das ende von path" ist gleich 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)))))))

Wenn graph ist ein fall von Graph , dann es gibt ein node1,node2,node3,arc1,arc2 der node1 ist ein teil von graph und node2 ist ein teil von graph und node3 ist ein teil von graph und arc1 ist ein teil von graph und arc2 ist ein teil von graph und node2 verbindet arc1 und node1 und node3 verbindet arc2 und node2 und node1 ist gleich node2 nicht und node2 ist gleich node3 nicht und node1 ist gleich node3 nicht und arc1 ist gleich arc2 nicht.

(=>
      (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)))))

Wenn graph ist ein fall von gerichtetes Graph und arc ist ein fall von Graphbogen und arc ist ein teil von graph , dann es gibt ein node1,node2 der "das ausgangsnullpunkt von arc" ist gleich node1 und "das terminalnullpunkt von arc" ist gleich node2 .

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

Wenn graph ist ein fall von Baumstruktur , dann es gibt kein Graphschleife loop der loop ist ein teil von graph .

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

wenn graph ist ein fall von Graphweg und arc ist ein fall von Graphbogen und arc ist ein teil von graph ,
dann wenn "das ausgangsnullpunkt von arc" ist gleich node , dann es gibt kein other der "das ausgangsnullpunkt von other" ist gleich node und other ist gleich arc nicht

(=>
      (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)))))))

wenn graph ist ein fall von Graphweg und arc ist ein fall von Graphbogen und arc ist ein teil von graph ,
dann wenn "das terminalnullpunkt von arc" ist gleich node , dann es gibt kein other der "das terminalnullpunkt von other" ist gleich node und other ist gleich arc nicht

(=>
      (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 ist ein fall von Multigraph nur wenn es gibt ein arc1,arc2,node1,node2 der arc1 ist ein teil von graph und arc2 ist ein teil von graph und node1 ist ein teil von graph und node2 ist ein teil von graph und arc1 verbindet node1 und node2 und arc2 verbindet node1 und node2 und arc1 ist gleich arc2 nicht.

(<=>
      (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 ist ein fall von Pseudograph nur wenn es gibt ein Graphschleife loop der loop ist ein teil von graph .

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

Wenn part ist ein fall von Graphelement , dann es gibt ein Graph graph der part ist ein teil von graph .

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

Wenn graph1 ist ein teilgraph von graph2 und element ist ein teil von graph1 , dann element ist ein teil von graph2 .

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

wenn
- "der wert von path" ist gleich sum
- subpath ist ein teilgraph von path
- arc1 ist ein teil von path
- der wert von arc1 ist number1
- für jeden arc2 gilt: wenn arc2 ist ein teil von path , dann arc2 ist ein teil von subpath oder arc2 ist gleich arc1
,
dann sum ist gleich "("der wert von 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)))

wenn
- "der wert von path" ist gleich sum
- arc1 ist ein teil von path
- arc2 ist ein teil von path
- der wert von arc1 ist number1
- der wert von arc2 ist number2
- für jeden arc3 gilt: wenn arc3 ist ein teil von path , dann arc3 ist gleich arc1 oder arc3 ist gleich arc2
,
dann "der wert von path" ist gleich "(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)))

Wenn path ist ein teil von graph und graph ist ein fall von gerichtetes Graph nicht, dann "die menge von Pfaden zwischen node1 und node2" ist gleich path nur wenn "die menge von Pfaden zwischen node2 und node1" ist gleich path .

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