  graphPart
|
|
Sigma KEE - graphPart
|
appearance as argument number 1
|
|
|
|
appearance as argument number 2
|
|
|
|
antecedent
|
|
|
(=>
(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))))))) |
Merge.kif 5750-5770 |
If All of the following hold: (1) X is an instance of graph (2) Y is an instance of graph node (3) Z is an instance of graph node (4) Y is a part of X (5) Z is a part of X (6) equal Y and Z, then All of the following hold: (1) there exist W (2) V such that W links Y (3) Z, V is a subgraph of X (4) V is an instance of graph path (5) equal the beginning of V (6) Y (7) equal the end of V (8) Z, or equal the beginning of V (9) Z (10) equal the end of V (11) Y |
(=>
(and
(instance ?GRAPH DirectedGraph)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(exists (?NODE1 ?NODE2)
(and
(equal
(InitialNodeFn ?ARC) ?NODE1)
(equal
(TerminalNodeFn ?ARC) ?NODE2)))) |
Merge.kif 5795-5803 |
If X is an instance of directed graph, Y is an instance of graph arc, and Y is a part of X, then there exist Z, W such that equal the starting node of Y, Z, equal the terminal node of Y, and W |
(=>
(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)))))) |
Merge.kif 5846-5857 |
If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the starting node of Y and Z, then there doesn't exist W such that equal the starting node of W, Z, equal W, and Y |
(=>
(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)))))) |
Merge.kif 5859-5870 |
If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the terminal node of Y and Z, then there doesn't exist W such that equal the terminal node of W, Z, equal W, and Y |
(=>
(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)))
(instance ?GRAPH MultiGraph)) |
Merge.kif 5910-5919 |
If All of the following hold: (1) X is a part of Y (2) Z is a part of Y (3) W is a part of Y (4) V is a part of Y (5) X links W and V (6) Z links W and V (7) equal X and Z, then Y is an instance of multi graph |
(=>
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH))
(instance ?GRAPH PseudoGraph)) |
Merge.kif 5933-5937 |
If X is an instance of graph loop and X is a part of Y, then Y is an instance of pseudo graph |
(=>
(and
(subGraph ?GRAPH1 ?GRAPH2)
(graphPart ?ELEMENT ?GRAPH1))
(graphPart ?ELEMENT ?GRAPH2)) |
Merge.kif 6024-6028 |
If X is a subgraph of Y and Z is a part of X, then Z is a part of Y |
(=>
(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))) |
Merge.kif 6098-6110 |
If equal the value of X and Y, Z is a subgraph of X, W is a part of X, the value of W is V, and For all GraphElement U: if U is a part of X, then U is a part of Z or equal U and W, then equal Y and (the value of Z and V) |
(=>
(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))) |
Merge.kif 6112-6125 |
If All of the following hold: (1) equal the value of X and Y (2) Z is a part of X (3) W is a part of X (4) the value of Z is V (5) the value of W is U (6) For all GraphElement T: if T is a part of X, then equal T and Z or equal T and W, then equal the value of X and (V and U) |
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(instance ?PATH
(GraphPathFn ?NODE1 ?NODE2))
(instance ?PATH
(GraphPathFn ?NODE2 ?NODE1)))) |
Merge.kif 6181-6187 |
If X is a part of Y and Y is not an instance of directed graph, then X is an instance of the set of paths between Z, W if, only if X is an instance of the set of paths between W, and Z |
(=>
(and
(graphMeasure ?G ?M)
(instance ?AN GraphNode)
(graphPart ?AN ?G)
(graphPart ?AA ?G)
(instance ?AA GraphArc)
(abstractCounterpart ?AN ?PN)
(abstractCounterpart ?AA ?PA)
(arcWeight ?AA ?N))
(measure ?PA
(MeasureFn ?N ?M))) |
Merge.kif 6284-6295 |
If All of the following hold: (1) X is the unit in Y (2) Z is an instance of graph node (3) Z is a part of Y (4) W is a part of Y (5) W is an instance of graph arc (6) the abstract counterpart of V is Z (7) the abstract counterpart of U is W (8) the value of W is T, then the measure of U is T X(s) |
|
consequent
|
|
|
(=>
(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 ?NODE1 ?NODE2 ?ARC1)
(links ?NODE2 ?NODE3 ?ARC2)
(not
(equal ?NODE1 ?NODE2))
(not
(equal ?NODE2 ?NODE3))
(not
(equal ?NODE1 ?NODE3))
(not
(equal ?ARC1 ?ARC2))))) |
Merge.kif 5772-5786 |
If X is an instance of graph, then All of the following hold: (1) there exist Y, Z,, , W,, , V (2) U such that Y is a part of X (3) Z is a part of X (4) W is a part of X (5) V is a part of X (6) U is a part of X (7) V links Y (8) Z (9) U links Z (10) W (11) equal Y (12) Z (13) equal Z (14) W (15) equal Y (16) W (17) equal V (18) U |
(=>
(instance ?GRAPH Tree)
(not
(exists (?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH))))) |
Merge.kif 5810-5816 |
If X is an instance of tree, then there doesn't exist Y such that Y is an instance of graph loop and Y is a part of X |
(=>
(instance ?GRAPH Tree)
(not
(exists (?LOOP)
(and
(instance ?LOOP GraphCircuit)
(graphPart ?LOOP ?GRAPH))))) |
Merge.kif 5818-5824 |
If X is an instance of tree, then there doesn't exist Y such that Y is an instance of graph circuit and Y is a part of X |
(=>
(instance ?GRAPH Tree)
(not
(exists (?ARC1 ?ARC2 ?NODE)
(and
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(graphPart ?NODE ?GRAPH)
(equal
(TerminalNodeFn ?ARC1) ?NODE)
(equal
(TerminalNodeFn ?ARC2) ?NODE)
(not
(equal ?ARC1 ?ARC2)))))) |
Merge.kif 5826-5836 |
If X is an instance of tree, then All of the following hold: (1) there don't exist Y, Z (2) W such that Y is a part of X (3) Z is a part of X (4) W is a part of X (5) equal the terminal node of Y (6) W (7) equal the terminal node of Z (8) W (9) equal Y (10) Z |
(=>
(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))))) |
Merge.kif 5897-5908 |
If X is an instance of multi graph, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is a part of X (3) Z is a part of X (4) W is a part of X (5) V is a part of X (6) Y links W (7) V (8) Z links W (9) V (10) equal Y (11) Z |
(=>
(instance ?GRAPH PseudoGraph)
(exists (?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH)))) |
Merge.kif 5926-5931 |
If X is an instance of pseudo graph, then there exists Y such that Y is an instance of graph loop and Y is a part of X |
(=>
(instance ?PART GraphElement)
(exists (?GRAPH)
(and
(instance ?GRAPH Graph)
(graphPart ?PART ?GRAPH)))) |
Merge.kif 5945-5950 |
If X is an instance of graph element, then there exists Y such that Y is an instance of graph and X is a part of Y |
(=>
(and
(subGraph ?GRAPH1 ?GRAPH2)
(graphPart ?ELEMENT ?GRAPH1))
(graphPart ?ELEMENT ?GRAPH2)) |
Merge.kif 6024-6028 |
If X is a subgraph of Y and Z is a part of X, then Z is a part of Y |
(=>
(graphMeasure ?G ?M)
(forall (?AC)
(and
(graphPart ?AC ?G)
(exists (?PC)
(abstractCounterpart ?AC ?PC))))) |
Merge.kif 6276-6282 |
If X is the unit in Y, then For all GraphElement Z: Z is a part of Y and there exists W such that the abstract counterpart of W is Z |
(=>
(and
(instance ?TS TransitSystem)
(instance ?T Transitway)
(abstractCounterpart ?G ?TS)
(systemPart ?T ?TS))
(exists (?GA)
(and
(instance ?GA GraphArc)
(abstractCounterpart ?GA ?T)
(graphPart ?GA ?G)))) |
Transportation.kif 3987-3997 |
If X is an instance of transit system, Y is an instance of transitway, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph arc, the abstract counterpart of Y is W, and W is a part of Z |
(=>
(and
(instance ?TS TransitSystem)
(instance ?TJ TransitwayJunction)
(abstractCounterpart ?G ?TS)
(systemPart ?TJ ?TS))
(exists (?GN)
(and
(instance ?GN GraphNode)
(abstractCounterpart ?GN ?TJ)
(graphPart ?GN ?G)))) |
Transportation.kif 3999-4009 |
If X is an instance of transit system, Y is an instance of transitway junction, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph node, the abstract counterpart of Y is W, and W is a part of Z |
|
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
