Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| EndNodeFn |
| appearance as argument number 1 |
|
| (instance EndNodeFn UnaryFunction) | Merge.kif 6070-6070 | End node is an instance of unary function |
| (instance EndNodeFn TotalValuedRelation) | Merge.kif 6071-6071 | End node is an instance of total valued relation |
| (domain EndNodeFn 1 GraphPath) | Merge.kif 6072-6072 | The number 1 argument of end node is an instance of graph path |
| (range EndNodeFn GraphNode) | Merge.kif 6073-6073 | The range of end node is an instance of graph node |
| (relatedInternalConcept EndNodeFn TerminalNodeFn) | Merge.kif 6074-6074 | End node is internally related to terminal node |
| (documentation EndNodeFn EnglishLanguage "A UnaryFunction that maps a GraphPath to the GraphNode that is the end of the GraphPath. Note that, unlike TerminalNodeFn (which relates a GraphArc to a GraphNode), EndNodeFn is a total function - every GraphPath has a end.") | Merge.kif 6076-6079 | End node is internally related to terminal node |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (and (equal (BeginNodeFn ?GRAPH) ?NODE) (equal (EndNodeFn ?GRAPH) ?NODE)) (instance ?GRAPH GraphCircuit)) |
Merge.kif 5885-5889 | If equal the beginning of X and Y and equal the end of X and Y, then X is an instance of graph circuit |
| 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 |
| (=> (instance ?GRAPH GraphCircuit) (exists (?NODE) (and (equal (BeginNodeFn ?GRAPH) ?NODE) (equal (EndNodeFn ?GRAPH) ?NODE)))) |
Merge.kif 5878-5883 | If X is an instance of graph circuit, then there exists Y such that equal the beginning of X, Y, equal the end of X, and 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 |
|