Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| PathWeightFn |
| appearance as argument number 1 |
|
| (instance PathWeightFn UnaryFunction) | Merge.kif 6090-6090 | Path weight is an instance of unary function |
| (domain PathWeightFn 1 GraphPath) | Merge.kif 6091-6091 | The number 1 argument of path weight is an instance of graph path |
| (range PathWeightFn RealNumber) | Merge.kif 6092-6092 | The range of path weight is an instance of real number |
| (documentation PathWeightFn EnglishLanguage "A UnaryFunction that maps a GraphPath to the sum of the arcWeights on the GraphArcs in the GraphPath.") | Merge.kif 6094-6096 | The range of path weight is an instance of real number |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (and (equal (PathWeightFn ?PATH) ?SUM) (subGraph ?SUBPATH ?PATH) (graphPart ?ARC1 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (forall (?ARC2) (=> (graphPart ?ARC2 ?PATH) (or (graphPart ?ARC2 ?SUBPATH) (equal ?ARC2 ?ARC1))))) (equal ?SUM (AdditionFn (PathWeightFn ?SUBPATH) ?NUMBER1))) |
Merge.kif 6098-6110 | If equal the value of X and Y, Z is a subgraph of X, W is a part of X, the value of W is V, and For all GraphElement U: if U is a part of X, then U is a part of Z or equal U and W, then equal Y and (the value of Z and V) |
| (=> (and (equal (PathWeightFn ?PATH) ?SUM) (graphPart ?ARC1 ?PATH) (graphPart ?ARC2 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (arcWeight ?ARC2 ?NUMBER2) (forall (?ARC3) (=> (graphPart ?ARC3 ?PATH) (or (equal ?ARC3 ?ARC1) (equal ?ARC3 ?ARC2))))) (equal (PathWeightFn ?PATH) (AdditionFn ?NUMBER1 ?NUMBER2))) |
Merge.kif 6112-6125 | If All of the following hold: (1) equal the value of X and Y (2) Z is a part of X (3) W is a part of X (4) the value of Z is V (5) the value of W is U (6) For all GraphElement T: if T is a part of X, then equal T and Z or equal T and W, then equal the value of X and (V and U) |
| (=> (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 |
|
|
| (=> (and (equal (PathWeightFn ?PATH) ?SUM) (subGraph ?SUBPATH ?PATH) (graphPart ?ARC1 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (forall (?ARC2) (=> (graphPart ?ARC2 ?PATH) (or (graphPart ?ARC2 ?SUBPATH) (equal ?ARC2 ?ARC1))))) (equal ?SUM (AdditionFn (PathWeightFn ?SUBPATH) ?NUMBER1))) |
Merge.kif 6098-6110 | If equal the value of X and Y, Z is a subgraph of X, W is a part of X, the value of W is V, and For all GraphElement U: if U is a part of X, then U is a part of Z or equal U and W, then equal Y and (the value of Z and V) |
| (=> (and (equal (PathWeightFn ?PATH) ?SUM) (graphPart ?ARC1 ?PATH) (graphPart ?ARC2 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (arcWeight ?ARC2 ?NUMBER2) (forall (?ARC3) (=> (graphPart ?ARC3 ?PATH) (or (equal ?ARC3 ?ARC1) (equal ?ARC3 ?ARC2))))) (equal (PathWeightFn ?PATH) (AdditionFn ?NUMBER1 ?NUMBER2))) |
Merge.kif 6112-6125 | If All of the following hold: (1) equal the value of X and Y (2) Z is a part of X (3) W is a part of X (4) the value of Z is V (5) the value of W is U (6) For all GraphElement T: if T is a part of X, then equal T and Z or equal T and W, then equal the value of X and (V and U) |
|