(=>
(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 |
(=>
(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 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 ?NODE GraphNode)
(exists (?OTHER ?ARC)
(links ?NODE ?OTHER ?ARC))) |
Merge.kif 5957-5960 |
If X is an instance of graph node, then there exist Y, Z such that Z links X, and Y |
(=>
(instance ?ARC GraphArc)
(exists (?NODE1 ?NODE2)
(links ?NODE1 ?NODE2 ?ARC))) |
Merge.kif 5967-5970 |
If X is an instance of graph arc, then there exist Y, Z such that X links Y, and Z |
(=>
(instance ?LOOP GraphLoop)
(exists (?NODE)
(links ?NODE ?NODE ?LOOP))) |
Merge.kif 5977-5980 |
If X is an instance of graph loop, then there exists Y such that X links Y and Y |
(=>
(links ?NODE1 ?NODE2 ?ARC)
(links ?NODE2 ?NODE1 ?ARC)) |
Merge.kif 6000-6002 |
If X links Y and Z, then X links Z and Y |
(=>
(and
(connects ?A ?NODE1 ?NODE2)
(abstractCounterpart ?N1 ?NODE1)
(abstractCounterpart ?N2 ?NODE2)
(abstractCounterpart ?ARC ?A))
(links ?N1 ?N2 ?ARC)) |
Transportation.kif 4011-4017 |
If X connects Y and Z, the abstract counterpart of Y is W, the abstract counterpart of Z is V, and the abstract counterpart of X is U, then U links W and V |
links