最大量路徑函數 (MaximalWeightedPathFn)

This BinaryFunction assigns two GraphNodes to the GraphPath with the largest sum of weighted arcs between the two GraphNodes.

Ontology

SUMO / GRAPH-THEORY

Class(es)

種類

可繼承關係

二元函數

最大量路徑函數

Coordinate term(s)

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

Type restrictions

圖路徑 MaximalWeightedPathFn(圖節點, 圖節點)

Axioms (2)

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))))