Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| subGraph |
| appearance as argument number 1 |
|
| (instance subGraph BinaryPredicate) | Merge.kif 6014-6014 | sub graph is an instance of binary predicate |
| (instance subGraph ReflexiveRelation) | Merge.kif 6015-6015 | sub graph is an instance of reflexive relation |
| (instance subGraph TransitiveRelation) | Merge.kif 6016-6016 | sub graph is an instance of transitive relation |
| (domain subGraph 1 Graph) | Merge.kif 6017-6017 | The number 1 argument of sub graph is an instance of graph |
| (domain subGraph 2 Graph) | Merge.kif 6018-6018 | The number 2 argument of sub graph is an instance of graph |
| (documentation subGraph EnglishLanguage "The relation between two Graphs when one Graph is a part of the other. (subGraph ?GRAPH1 ?GRAPH2) means that ?GRAPH1 is a part of ?GRAPH2.") | Merge.kif 6020-6022 | The number 2 argument of sub graph is an instance of graph |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage subGraph "sub graph") | domainEnglishFormat.kif 55723-55723 | |
| (termFormat ChineseTraditionalLanguage subGraph "子圖") | domainEnglishFormat.kif 55724-55724 | |
| (termFormat ChineseLanguage subGraph "子图") | domainEnglishFormat.kif 55725-55725 | |
| (format EnglishLanguage subGraph "%1 is %n a subgraph of %2") | english_format.kif 753-753 |
| antecedent |
|
|
| (=> (and (subGraph ?GRAPH1 ?GRAPH2) (graphPart ?ELEMENT ?GRAPH1)) (graphPart ?ELEMENT ?GRAPH2)) |
Merge.kif 6024-6028 | If X is a subgraph of Y and Z is a part of X, then Z is a part of Y |
| (=> (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) |
| 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 |
| (=> (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 |
|