| GraphPathFn |
| appearance as argument number 1 |
|
|
| (instance GraphPathFn BinaryFunction) | Merge.kif 6101-6101 | Graph path is an instance of binary function |
| (instance GraphPathFn TotalValuedRelation) | Merge.kif 6102-6102 | Graph path is an instance of total valued relation |
| (domain GraphPathFn 1 GraphNode) | Merge.kif 6103-6103 | The number 1 argument of graph path is an instance of graph node |
| (domain GraphPathFn 2 GraphNode) | Merge.kif 6104-6104 | The number 2 argument of graph path is an instance of graph node |
| (rangeSubclass GraphPathFn GraphPath) | Merge.kif 6105-6105 | 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 6107-6109 | 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 6071-6077 | 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 6093-6099 | 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 6067-6069 | 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 6089-6091 | 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 6111-6117 | 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 |
|
|