路徑量函數 (PathWeightFn)

A UnaryFunction that maps a GraphPath to the sum of the arcWeights on the GraphArcs in the GraphPath.

Ontology

SUMO / GRAPH-THEORY

Class(es)

種類

可繼承關係

一元函數

路徑量函數

Coordinate term(s)

絕對值函數描述函數弧餘弦弧正弦弧正切反面函數（時間）開始函數最初節點函數計數函數上限函數互補函數餘弦函數相交路徑函數單位函數（時間）結束函式最後節點函數範圍函數下限函數正面函數（時間）未來函式概化函數概化聯集函數十億計函數虛數函數最近未來時間函數最近過去時間函數起始節點函數整數平方根函數千計函數列長函數級數函數百萬計函數百萬分之一計函數千分之一計函數最小相交路徑函數奈米函數分子函數組織函數過去時間函式兆分之一計函數冪集合函數前數函數主體函數或然率函數特性函數有理數函數實數函數倒數函數整數函數正負號函數正弦函數表皮函數平方根函數後數函數正切函數兆計函數終節點函數財產函數存在時間函數年份函數

Type restrictions

實數 PathWeightFn(圖路徑)

Axioms (4)

if
- "path 的路�|長量值" 等於 sum
- subpath 是 path 的次圖
- arc1 是 path 的部分
- arc1 的弧線量是 number1
- for all arc2 holds: if arc2 是 path 的部分, then arc2 是 subpath 的部分 or arc2 等於 arc1
,
then sum 等於 "("subpath 的路�|長量值"+number1)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))

if
- "path 的路�|長量值" 等於 sum
- arc1 是 path 的部分
- arc2 是 path 的部分
- arc1 的弧線量是 number1
- arc2 的弧線量是 number2
- for all arc3 holds: if arc3 是 path 的部分, then arc3 等於 arc1 or arc3 等於 arc2
,
then "path 的路�|長量值" 等於 "(number1+number2)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (graphPart ?ARC1 ?PATH)
            (graphPart ?ARC2 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (arcWeight ?ARC2 ?NUMBER2)
            (forall
                  (?ARC3)
                  (=>
                        (graphPart ?ARC3 ?PATH)
                        (or
                              (equal ?ARC3 ?ARC1)
                              (equal ?ARC3 ?ARC2)))))
      (equal
            (PathWeightFn ?PATH)
            (AdditionFn ?NUMBER1 ?NUMBER2)))

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