Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
 |
   GraphPath
|
|
|
| appearance as argument number 1 |
|
|
| (subclass GraphPath DirectedGraph) | Merge.kif 5838-5838 | Graph path is a subclass of directed graph |
| (documentation GraphPath EnglishLanguage "Informally, a single, directed route between two GraphNodes in a Graph. Formally, a DirectedGraph that is a subGraph of the original Graph and such that no two GraphArcs in the DirectedGraph have the same initial node (see InitialNodeFn) or the same terminal node (see TerminalNodeFn).") | Merge.kif 5840-5844 | Graph path is a subclass of directed graph |
| appearance as argument number 2 |
|
|
| (subclass GraphCircuit GraphPath) | Merge.kif 5872-5872 | Graph circuit is a subclass of graph path |
| (range MinimalWeightedPathFn GraphPath) | Merge.kif 6131-6131 | The range of minimal weighted path is an instance of graph path |
| (range MaximalWeightedPathFn GraphPath) | Merge.kif 6153-6153 | The range of maximal weighted path is an instance of graph path |
| (rangeSubclass GraphPathFn GraphPath) | Merge.kif 6175-6175 | The values returned by graph path are subclasses of graph path |
| (rangeSubclass CutSetFn GraphPath) | Merge.kif 6191-6191 | The values returned by cut set are subclasses of graph path |
| (rangeSubclass MinimalCutSetFn GraphPath) | Merge.kif 6199-6199 | The values returned by minimal cut set are subclasses of graph path |
| (termFormat EnglishLanguage GraphPath "graph path") | english_format.kif 1083-1083 | The values returned by minimal cut set are subclasses of graph path |
| appearance as argument number 3 |
|
|
| (domain pathLength 1 GraphPath) | Merge.kif 6031-6031 | The number 1 argument of path length is an instance of graph path |
| (domain BeginNodeFn 1 GraphPath) | Merge.kif 6061-6061 | The number 1 argument of begin node is an instance of graph path |
| (domain EndNodeFn 1 GraphPath) | Merge.kif 6072-6072 | The number 1 argument of end node is an instance of graph path |
| (domain PathWeightFn 1 GraphPath) | Merge.kif 6091-6091 | The number 1 argument of path weight is an instance of graph path |
| 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 (instance ?GRAPH GraphPath) (instance ?ARC GraphArc) (graphPart ?ARC ?GRAPH) (equal (TerminalNodeFn ?ARC) ?NODE)) (not (exists (?OTHER) (and (equal (TerminalNodeFn ?OTHER) ?NODE) (not (equal ?OTHER ?ARC)))))) |
Merge.kif 5859-5870 | If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the terminal node of Y and Z, then there doesn't exist W such that equal the terminal node of W, Z, equal W, and Y |
| 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 |
| (=> (distanceOnPath ?DIST ?PATH) (exists (?GP) (and (instance ?GP GraphPath) (abstractCounterpart ?GP ?PATH)))) |
Transportation.kif 3940-3945 | If the distance of X is Y, then there exists Z such that Z is an instance of graph path and the abstract counterpart of X is Z |
|