圖路徑函數 (GraphPathFn)

A BinaryFunction that maps two GraphNodes to the Class of GraphPaths between those two nodes. Note that the two GraphNodes must belong to the same Graph.

Ontology

SUMO / GRAPH-THEORY

Class(es)

種類

可繼承關係

二元函數

圖路徑函數

Coordinate term(s)

加法函數日函數密度函數除法函數（文本）版本函數指數函數小時函數交集函數間隔函數種類描述函數列結函數列序函數對數函數最大值函數最大量路徑函數測量函數部分整體差異函數部分整體交集函數部分整體加總函數最小值函數最小量路徑函數分鐘函數月份函數乘法函數期刊一期函數週期性時距函數關係互補函數相對時間函數餘數函數秒鐘函數系列一卷函數速度函數減法函數時間單位函數時間歷程函數聯集函數位置函數

Type restrictions

subclass 圖路徑 GraphPathFn(圖節點, 圖節點)

Axioms (5)

If "最小量路徑函數(node1,node2)" 等於 path, then path 是 "node1 和 node2 間集合路�|" 的實例.

(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "最小量路徑函數(node1,node2)" 等於 path and "path 的路�|長量值" 等於 number,
then for all path2 holds: if path2 是 "node1 和 node2 間集合路�|" 的實例 and "path2 的路�|長量值" 等於 number2, then number2 大於或等於 number1

(=>
      (and
            (equal
                  (MinimalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If "node1 和 node2 間最大路�|" 等於 path, then path 是 "node1 和 node2 間集合路�|" 的實例.

(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "node1 和 node2 間最大路�|" 等於 path and "path 的路�|長量值" 等於 number,
then for all path2 holds: if path2 是 "node1 和 node2 間集合路�|" 的實例 and "path2 的路�|長量值" 等於 number2, then number2 小於或等於 number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If path 是 graph 的部分 and graph 是有向圖的實例, then "node1 和 node2 間集合路�|" 等於 path if and only if "node2 和 node1 間集合路�|" 等於 path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))