Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| BeginNodeFn |
| appearance as argument number 1 |
|
| (instance BeginNodeFn UnaryFunction) | Merge.kif 6059-6059 | Begin node is an instance of unary function |
| (instance BeginNodeFn TotalValuedRelation) | Merge.kif 6060-6060 | Begin node is an instance of total valued relation |
| (domain BeginNodeFn 1 GraphPath) | Merge.kif 6061-6061 | The number 1 argument of begin node is an instance of graph path |
| (range BeginNodeFn GraphNode) | Merge.kif 6062-6062 | The range of begin node is an instance of graph node |
| (relatedInternalConcept BeginNodeFn InitialNodeFn) | Merge.kif 6063-6063 | Begin node is internally related to initial node |
| (documentation BeginNodeFn EnglishLanguage "A UnaryFunction that maps a GraphPath to the GraphNode that is the beginning of the GraphPath. Note that, unlike InitialNodeFn (which relates a GraphArc to a GraphNode), BeginNodeFn is a total function - every GraphPath has a beginning.") | Merge.kif 6065-6068 | Begin node is internally related to initial node |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage BeginNodeFn "begin node") | domainEnglishFormat.kif 10575-10575 | |
| (termFormat ChineseTraditionalLanguage BeginNodeFn "開始節點") | domainEnglishFormat.kif 10576-10576 | |
| (termFormat ChineseLanguage BeginNodeFn "开始节点") | domainEnglishFormat.kif 10577-10577 | |
| (format EnglishLanguage BeginNodeFn "the beginning of %1") | english_format.kif 765-765 |
| antecedent |
|
|
| (=> (and (equal (BeginNodeFn ?GRAPH) ?NODE) (equal (EndNodeFn ?GRAPH) ?NODE)) (instance ?GRAPH GraphCircuit)) |
Merge.kif 5885-5889 | If equal the beginning of X and Y and equal the end of X and Y, then X is an instance of graph circuit |
| consequent |
|
|
| (=> (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 GraphCircuit) (exists (?NODE) (and (equal (BeginNodeFn ?GRAPH) ?NODE) (equal (EndNodeFn ?GRAPH) ?NODE)))) |
Merge.kif 5878-5883 | If X is an instance of graph circuit, then there exists Y such that equal the beginning of X, Y, equal the end of X, and Y |
| (=> (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 |
|