Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - PathWeightFn
PathWeightFn

appearance as argument number 1
-------------------------


s__documentation(s__PathWeightFn__m,s__ChineseLanguage,'"这是一个 UnaryFunction, 它把一个 GraphPath 联系到在这条 GraphPath GraphArcs 上的 arcWeight 总和。"')

chinese_format.kif 2370-2371
s__documentation(s__PathWeightFn__m,s__EnglishLanguage,'"A UnaryFunction that maps a GraphPath to the sum of the arcWeights on the GraphArcs in the GraphPath."')

Merge.kif 5620-5622
s__domain(s__PathWeightFn__m,n__1,s__GraphPath)

Merge.kif 5617-5617 The number 1 argument of path weight is an instance of graph path
s__instance(s__UnaryFunction,s__SetOrClass)

s__instance(s__PathWeightFn__m,s__UnaryFunction)

Merge.kif 5616-5616 Path weight is an instance of unary function
s__range(s__PathWeightFn__m,s__Quantity)

Merge.kif 5618-5618 The range of path weight is an instance of quantity

appearance as argument number 2
-------------------------


s__format(s__ChineseLanguage,s__PathWeightFn__m,'"%1 的值"')

chinese_format.kif 769-769
s__format(s__EnglishLanguage,s__PathWeightFn__m,'"the value of %1"')

english_format.kif 772-772
s__termFormat(s__ChineseLanguage,s__PathWeightFn__m,'"路径衡量函数"')

chinese_format.kif 770-770
s__termFormat(s__ChineseLanguage,s__PathWeightFn__m,'"路径重量"')

domainEnglishFormat.kif 44683-44683
s__termFormat(s__ChineseTraditionalLanguage,s__PathWeightFn__m,'"路徑重量"')

domainEnglishFormat.kif 44682-44682
s__termFormat(s__EnglishLanguage,s__PathWeightFn__m,'"path weight"')

domainEnglishFormat.kif 44681-44681

antecedent
-------------------------


( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   ((s__instance(V__NODE2,s__GraphNode) &
       s__instance(V__NODE1,s__GraphNode) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__MaximalWeightedPathFn(V__NODE1,V__NODE2)
       = V__PATH)
     &
     (s__PathWeightFn(V__PATH)
     = V__NUMBER1))
=>
( ! [V__PATH2] :
   (s__instance(V__PATH2,s__GraphPath) =>
     (s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
   &
   (s__PathWeightFn(V__PATH2)
   = V__NUMBER2))
=>
s__lessThanOrEqualTo(V__NUMBER2,V__NUMBER1)))
)
)

Merge.kif 5692-5701
( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   ((s__instance(V__NODE2,s__GraphNode) &
       s__instance(V__NODE1,s__GraphNode) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__MinimalWeightedPathFn(V__NODE1,V__NODE2)
       = V__PATH)
     &
     (s__PathWeightFn(V__PATH)
     = V__NUMBER1))
=>
( ! [V__PATH2] :
   (s__instance(V__PATH2,s__GraphPath) =>
     (s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
   &
   (s__PathWeightFn(V__PATH2)
   = V__NUMBER2))
=>
s__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1)))
)
)

Merge.kif 5667-5676
( ! [V__SUM,V__NUMBER1,V__NUMBER2,V__ARC1,V__PATH,V__ARC2] :
   ((s__instance(V__SUM,s__Quantity) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__ARC1,s__GraphArc) &
       s__instance(V__PATH,s__GraphPath) &
       s__instance(V__ARC2,s__GraphArc))
     =>
     ((s__PathWeightFn(V__PATH)
       = V__SUM)
     &
     s__graphPart(V__ARC1,V__PATH)
   &
   s__graphPart(V__ARC2,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
s__arcWeight(V__ARC2,V__NUMBER2)
&
( ! [V__ARC3] :
(s__instance(V__ARC3,s__GraphElement) =>
s__graphPart(V__ARC3,V__PATH)
=>
((V__ARC3 = V__ARC1)
|
(V__ARC3 = V__ARC2)))))
=>
(s__PathWeightFn(V__PATH)
= s__AdditionFn(V__NUMBER1,V__NUMBER2))
)
)

Merge.kif 5638-5651
( ! [V__SUM,V__NUMBER1,V__SUBPATH,V__ARC1,V__PATH] :
   ((s__instance(V__SUM,s__Quantity) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__SUBPATH,s__GraphPath) &
       s__instance(V__ARC1,s__GraphArc) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__PathWeightFn(V__PATH)
       = V__SUM)
     &
     s__subGraph(V__SUBPATH,V__PATH)
   &
   s__graphPart(V__ARC1,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
( ! [V__ARC2] :
(s__instance(V__ARC2,s__GraphElement) =>
   s__graphPart(V__ARC2,V__PATH)
=>
(s__graphPart(V__ARC2,V__SUBPATH)
|
(V__ARC2 = V__ARC1)))))
=>
(V__SUM = s__AdditionFn(s__PathWeightFn(V__SUBPATH)
,V__NUMBER1))
)
)

Merge.kif 5624-5636

consequent
-------------------------


( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   ((s__instance(V__NODE2,s__GraphNode) &
       s__instance(V__NODE1,s__GraphNode) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__MaximalWeightedPathFn(V__NODE1,V__NODE2)
       = V__PATH)
     &
     (s__PathWeightFn(V__PATH)
     = V__NUMBER1))
=>
( ! [V__PATH2] :
   (s__instance(V__PATH2,s__GraphPath) =>
     (s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
   &
   (s__PathWeightFn(V__PATH2)
   = V__NUMBER2))
=>
s__lessThanOrEqualTo(V__NUMBER2,V__NUMBER1)))
)
)

Merge.kif 5692-5701
( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   ((s__instance(V__NODE2,s__GraphNode) &
       s__instance(V__NODE1,s__GraphNode) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__MinimalWeightedPathFn(V__NODE1,V__NODE2)
       = V__PATH)
     &
     (s__PathWeightFn(V__PATH)
     = V__NUMBER1))
=>
( ! [V__PATH2] :
   (s__instance(V__PATH2,s__GraphPath) =>
     (s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
   &
   (s__PathWeightFn(V__PATH2)
   = V__NUMBER2))
=>
s__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1)))
)
)

Merge.kif 5667-5676
( ! [V__SUM,V__NUMBER1,V__NUMBER2,V__ARC1,V__PATH,V__ARC2] :
   ((s__instance(V__SUM,s__Quantity) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__NUMBER2,s__Quantity) &
       s__instance(V__ARC1,s__GraphArc) &
       s__instance(V__PATH,s__GraphPath) &
       s__instance(V__ARC2,s__GraphArc))
     =>
     ((s__PathWeightFn(V__PATH)
       = V__SUM)
     &
     s__graphPart(V__ARC1,V__PATH)
   &
   s__graphPart(V__ARC2,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
s__arcWeight(V__ARC2,V__NUMBER2)
&
( ! [V__ARC3] :
(s__instance(V__ARC3,s__GraphElement) =>
s__graphPart(V__ARC3,V__PATH)
=>
((V__ARC3 = V__ARC1)
|
(V__ARC3 = V__ARC2)))))
=>
(s__PathWeightFn(V__PATH)
= s__AdditionFn(V__NUMBER1,V__NUMBER2))
)
)

Merge.kif 5638-5651
( ! [V__SUM,V__NUMBER1,V__SUBPATH,V__ARC1,V__PATH] :
   ((s__instance(V__SUM,s__Quantity) &
       s__instance(V__NUMBER1,s__Quantity) &
       s__instance(V__SUBPATH,s__GraphPath) &
       s__instance(V__ARC1,s__GraphArc) &
       s__instance(V__PATH,s__GraphPath))
     =>
     ((s__PathWeightFn(V__PATH)
       = V__SUM)
     &
     s__subGraph(V__SUBPATH,V__PATH)
   &
   s__graphPart(V__ARC1,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
( ! [V__ARC2] :
(s__instance(V__ARC2,s__GraphElement) =>
   s__graphPart(V__ARC2,V__PATH)
=>
(s__graphPart(V__ARC2,V__SUBPATH)
|
(V__ARC2 = V__ARC1)))))
=>
(V__SUM = s__AdditionFn(s__PathWeightFn(V__SUBPATH)
,V__NUMBER1))
)
)

Merge.kif 5624-5636


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners