Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| GraphPathFn |
| appearance as argument number 1 |
|
| (instance GraphPathFn BinaryFunction) | Merge.kif 6171-6171 | Graph path is an instance of binary function |
| (instance GraphPathFn TotalValuedRelation) | Merge.kif 6172-6172 | Graph path is an instance of total valued relation |
| (domain GraphPathFn 1 GraphNode) | Merge.kif 6173-6173 | The number 1 argument of graph path is an instance of graph node |
| (domain GraphPathFn 2 GraphNode) | Merge.kif 6174-6174 | The number 2 argument of graph path is an instance of graph node |
| (rangeSubclass GraphPathFn GraphPath) | Merge.kif 6175-6175 | The values returned by graph path are subclasses of graph path |
| (documentation GraphPathFn EnglishLanguage "A BinaryFunction that maps two GraphNodes to the Class of GraphPaths between those two nodes. Note that the two GraphNodes must belong to the same Graph.") | Merge.kif 6177-6179 | The values returned by graph path are subclasses of graph path |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage GraphPathFn "graph path") | domainEnglishFormat.kif 26468-26468 | |
| (termFormat ChineseTraditionalLanguage GraphPathFn "圖形路徑") | domainEnglishFormat.kif 26469-26469 | |
| (termFormat ChineseLanguage GraphPathFn "图形路径") | domainEnglishFormat.kif 26470-26470 | |
| (format EnglishLanguage GraphPathFn "the set of paths between %1 and %2") | english_format.kif 775-775 |
| antecedent |
|
|
| (=> (and (equal (MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH) (equal (PathWeightFn ?PATH) ?NUMBER1) (instance ?PATH2 (GraphPathFn ?NODE1 ?NODE2)) (equal (PathWeightFn ?PATH2) ?NUMBER2)) (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1)) |
Merge.kif 6141-6147 | If equal the lowest cost path between X, Y, and Z, equal the value of Z and W, V is an instance of the set of paths between X and Y, and equal the value of V and U, then U is greater than or equal to W |
| (=> (and (equal (MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH) (equal (PathWeightFn ?PATH) ?NUMBER1) (instance ?PATH2 (GraphPathFn ?NODE1 ?NODE2)) (equal (PathWeightFn ?PATH2) ?NUMBER2)) (lessThanOrEqualTo ?NUMBER2 ?NUMBER1)) |
Merge.kif 6163-6169 | If equal the highest cost path between X, Y, and Z, equal the value of Z and W, V is an instance of the set of paths between X and Y, and equal the value of V and U, then U is less than or equal to W |
| consequent |
|
|
| (=> (equal (MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH) (instance ?PATH (GraphPathFn ?NODE1 ?NODE2))) |
Merge.kif 6137-6139 | If equal the lowest cost path between X, Y, and Z, then Z is an instance of the set of paths between X and Y |
| (=> (equal (MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH) (instance ?PATH (GraphPathFn ?NODE1 ?NODE2))) |
Merge.kif 6159-6161 | If equal the highest cost path between X, Y, and Z, then Z is an instance of the set of paths between X and Y |
| (=> (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 |
|