(=>
(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 |
(=>
(distanceOnPath ?DIST ?PATH)
(exists (?GP)
(and
(instance ?GP GraphPath)
(abstractCounterpart ?GP ?PATH)))) |
Transportation.kif 3940-3945 |
If the distance of X is Y, then there exists Z such that Z is an instance of graph path and the abstract counterpart of X is Z |
(=>
(and
(distanceOnPath ?DIST ?PATH)
(pathInSystem ?PATH ?SYS)
(routeStart ?START ?PATH)
(routeEnd ?END ?PATH)
(abstractCounterpart ?GRAPH ?SYS))
(exists (?S ?BN ?EN)
(and
(subGraph ?S ?GRAPH)
(equal ?BN
(BeginNodeFn ?GRAPH))
(equal ?EN
(EndNodeFn ?GRAPH))
(abstractCounterpart ?BN ?START)
(abstractCounterpart ?EN ?END)))) |
Transportation.kif 3947-3960 |
If the distance of X is Y, Z is a path in system of X, W is the start of X, V is the end of X, and the abstract counterpart of Z is U, then All of the following hold: (1) there exist T, S (2) R such that T is a subgraph of U (3) equal S (4) the beginning of U (5) equal R (6) the end of U (7) the abstract counterpart of W is S (8) the abstract counterpart of V is R |
(=>
(instance ?TS TransitSystem)
(exists (?G)
(and
(instance ?G Graph)
(abstractCounterpart ?G ?TS)))) |
Transportation.kif 3980-3985 |
If X is an instance of transit system, then there exists Y such that Y is an instance of graph and the abstract counterpart of X is Y |
(=>
(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 |
