  GraphPathFn
|
|
Sigma KEE - GraphPathFn
|
appearance as argument number 1
|
|
|
|
appearance as argument number 2
|
|
|
|
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 |
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
