Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| routeStart |
| appearance as argument number 1 |
|
| (instance routeStart BinaryPredicate) | Transportation.kif 3894-3894 | route start is an instance of binary predicate |
| (domain routeStart 1 Region) | Transportation.kif 3895-3895 | The number 1 argument of route start is an instance of region |
| (domain routeStart 2 TransitSystem) | Transportation.kif 3896-3896 | The number 2 argument of route start is an instance of transit system |
| (documentation routeStart EnglishLanguage "(routeStart ?REGION ?SYSTEM) means that within the given ?SYSTEM the given ?REGION is connected to only one other Region.") | Transportation.kif 3897-3899 | The number 2 argument of route start is an instance of transit system |
| appearance as argument number 2 |
|
|
| (format EnglishLanguage routeStart "%1 is the start of %2") | domainEnglishFormat.kif 4460-4460 | |
| (format ChineseTraditionalLanguage routeStart "%1 是 %2 的 start ") | domainEnglishFormat.kif 4461-4461 | |
| (format ChineseLanguage routeStart "%1 是 %2 的 start ") | domainEnglishFormat.kif 4462-4462 | |
| (termFormat EnglishLanguage routeStart "route start") | domainEnglishFormat.kif 65964-65964 |
| antecedent |
|
|
| (=> (routeStart ?R ?TS) (exists (?T) (and (instance ?T Transitway) (connected ?R ?T) (systemPart ?T ?TS) (not (exists (?T2) (and (instance ?T2 Transitway) (connected ?R ?T2) (systemPart ?T2 ?TS) (not (equal ?T ?T2)))))))) |
Transportation.kif 3901-3915 | If X is the start of Y, then All of the following hold: (1) there exists Z such that Z is an instance of transitway (2) X is connected to Z (3) Y is a system part of Z (4) there doesn't exist W such that W is an instance of transitway (5) X is connected to W (6) Y is a system part of W (7) equal Z (8) W |
| (=> (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 |
|