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.

Ontology

SUMO / GRAPH-THEORY

Class(es)

Classe

inheritable relation

PredicatoBinario
is instance of

RelazioneAsimmetrica
is instance of

RelazioneNonRiflessiva
is instance of

graph part

Coordinate term(s)

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

Type restrictions

graphPart(ElementoDelGrafo, Grafo)

Axioms (13)

Se graph é un' istanza di Grafo e node1 é un' istanza di NodoDelGrafo e node2 é un' istanza di NodoDelGrafo e node1 é una parte di graph e node2 é una parte di graph e node1 is not uguale a node2, allora esiste arc,path tale che

arc legas node1 e node2
- path é un sottografo di graph
- path é un' istanza di CamminoDelGrafo
- - "l' inizio di path" is uguale a node1 e "la fine di path" is uguale a node2
  - "l' inizio di path" is uguale a node2 e "la fine di path" is uguale a 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)))))))

Se graph é un' istanza di Grafo, allora esiste node1,node2,node3,arc1,arc2 tale che node1 é una parte di graph e node2 é una parte di graph e node3 é una parte di graph e arc1 é una parte di graph e arc2 é una parte di graph e node2 legas arc1 e node1 e node3 legas arc2 e node2 e node1 is not uguale a node2 e node2 is not uguale a node3 e node1 is not uguale a node3 e arc1 is not uguale a 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)))))

Se graph é un' istanza di GrafoDiretto e arc é un' istanza di ArcoDelGrafo e arc é una parte di graph, allora esiste node1,node2 tale che "il nodo iniziale di arc" is uguale a node1 e "il nodo terminale di arc" is uguale a node2.

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

Se graph é un' istanza di Albero, allora non esiste GrafoCiclico loop tale che loop é una parte di graph.

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

se graph é un' istanza di CamminoDelGrafo e arc é un' istanza di ArcoDelGrafo e arc é una parte di graph,
allora se "il nodo iniziale di arc" is uguale a node, allora non esiste other tale che "il nodo iniziale di other" is uguale a node e other is not uguale a 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)))))))

se graph é un' istanza di CamminoDelGrafo e arc é un' istanza di ArcoDelGrafo e arc é una parte di graph,
allora se "il nodo terminale di arc" is uguale a node, allora non esiste other tale che "il nodo terminale di other" is uguale a node e other is not uguale a 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 é un' istanza di MultiGrafo se e solo se esiste arc1,arc2,node1,node2 tale che arc1 é una parte di graph e arc2 é una parte di graph e node1 é una parte di graph e node2 é una parte di graph e arc1 legas node1 e node2 e arc2 legas node1 e node2 e arc1 is not uguale a 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 é un' istanza di PseudoGrafo se e solo se esiste GrafoCiclico loop tale che loop é una parte di graph.

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

Se part é un' istanza di ElementoDelGrafo, allora esiste Grafo graph tale che part é una parte di graph.

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

Se graph1 é un sottografo di graph2 e element é una parte di graph1, allora element é una parte di graph2.

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

se
- "il valore di path" is uguale a sum
- subpath é un sottografo di path
- arc1 é una parte di path
- il valore diarc1 énumber1
- per ogni arc2 vale: se arc2 é una parte di path, allora arc2 é una parte di subpath o arc2 is uguale a arc1
,
allora sum is uguale a "("il valore di 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)))

se
- "il valore di path" is uguale a sum
- arc1 é una parte di path
- arc2 é una parte di path
- il valore diarc1 énumber1
- il valore diarc2 énumber2
- per ogni arc3 vale: se arc3 é una parte di path, allora arc3 is uguale a arc1 o arc3 is uguale a arc2
,
allora "il valore di path" is uguale a "(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)))

Se path é una parte di graph e graph é not un' istanza di GrafoDiretto, allora "l' insieme di cammini tra node1 e node2" is uguale a path se e solo se "l' insieme di cammini tra node2 e node1" is uguale a path.

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