Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| InitialNodeFn |
| appearance as argument number 1 |
|
| (instance InitialNodeFn UnaryFunction) | Merge.kif 6039-6039 | Initial node is an instance of unary function |
| (instance InitialNodeFn PartialValuedRelation) | Merge.kif 6040-6040 | Initial node is an instance of partial valued relation |
| (domain InitialNodeFn 1 GraphArc) | Merge.kif 6041-6041 | The number 1 argument of initial node is an instance of graph arc |
| (range InitialNodeFn GraphNode) | Merge.kif 6042-6042 | The range of initial node is an instance of graph node |
| (documentation InitialNodeFn EnglishLanguage "A UnaryFunction that maps a GraphArc to the initial node of the GraphArc. Note that this is a partial function. In particular, the function is undefined for GraphArcs that are not part of a DirectedGraph.") | Merge.kif 6044-6047 | The range of initial node is an instance of graph node |
| appearance as argument number 2 |
|
|
| (relatedInternalConcept BeginNodeFn InitialNodeFn) | Merge.kif 6063-6063 | Begin node is internally related to initial node |
| (termFormat EnglishLanguage InitialNodeFn "initial node") | domainEnglishFormat.kif 30123-30123 | Begin node is internally related to initial node |
| (termFormat ChineseTraditionalLanguage InitialNodeFn "初始節點") | domainEnglishFormat.kif 30124-30124 | Begin node is internally related to initial node |
| (termFormat ChineseLanguage InitialNodeFn "初始节点") | domainEnglishFormat.kif 30125-30125 | Begin node is internally related to initial node |
| (format EnglishLanguage InitialNodeFn "the starting node of %1") | english_format.kif 761-761 | Begin node is internally related to initial node |
| antecedent |
|
|
| (=> (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc) (graphPart ?ARC ?GRAPH) (equal (InitialNodeFn ?ARC) ?NODE)) (not (exists (?OTHER) (and (equal (InitialNodeFn ?OTHER) ?NODE) (not (equal ?OTHER ?ARC)))))) |
Merge.kif 5846-5857 | If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the starting node of Y and Z, then there doesn't exist W such that equal the starting node of W, Z, equal W, and Y |
| (=> (and (equal (InitialNodeFn ?ARC) ?NODE) (equal (TerminalNodeFn ?ARC) ?NODE)) (instance ?ARC GraphLoop)) |
Merge.kif 5986-5990 | If equal the starting node of X and Y and equal the terminal node of X and Y, then X is an instance of graph loop |
| consequent |
|
|
| (=> (and (instance ?GRAPH DirectedGraph) (instance ?ARC GraphArc) (graphPart ?ARC ?GRAPH)) (exists (?NODE1 ?NODE2) (and (equal (InitialNodeFn ?ARC) ?NODE1) (equal (TerminalNodeFn ?ARC) ?NODE2)))) |
Merge.kif 5795-5803 | If X is an instance of directed graph, Y is an instance of graph arc, and Y is a part of X, then there exist Z, W such that equal the starting node of Y, Z, equal the terminal node of Y, and W |
| (=> (and (instance ?GRAPH GraphPath) (instance ?ARC GraphArc) (graphPart ?ARC ?GRAPH) (equal (InitialNodeFn ?ARC) ?NODE)) (not (exists (?OTHER) (and (equal (InitialNodeFn ?OTHER) ?NODE) (not (equal ?OTHER ?ARC)))))) |
Merge.kif 5846-5857 | If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the starting node of Y and Z, then there doesn't exist W such that equal the starting node of W, Z, equal W, and Y |
|