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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - AssignmentFn
AssignmentFn

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


s__documentation(s__AssignmentFn__m,s__ChineseLanguage,'如果F是一个 Function,它所代表物体的值以 N1,...,NK表示, 那么 (AssignmentFn F N1 ... NK) 就是应用F到这些物体以N1,..., NK所代表的值。 在其他情况下,这个值是没有被下定义的。')

Merge.kif 813-815
s__documentation(s__AssignmentFn__m,s__EnglishLanguage,'If F is a Function with a value for the objects denoted by N1,..., NK, then (AssignmentFn F N1 ... NK) is the value of applying F to the objects denoted by N1,..., NK. Otherwise, the value is undefined.')

Merge.kif 809-812
s__domain(s__AssignmentFn__m,1,s__Function)

Merge.kif 806-806 The number 1 argument of assignment is an instance of function
s__domain(s__AssignmentFn__m,2,s__Entity)

Merge.kif 807-807 The number 2 argument of assignment is an instance of entity
s__instance(s__Function,s__SetOrClass)

s__instance(s__AssignmentFn__m,s__Function)

Merge.kif 804-804 Assignment is an instance of function
s__instance(s__AssignmentFn__m,s__VariableArityRelation)

s__instance(s__VariableArityRelation,s__SetOrClass)

Merge.kif 805-805 Assignment is an instance of variable arity relation
s__range(s__AssignmentFn__m,s__Entity)

Merge.kif 808-808 The range of assignment is an instance of entity

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


s__format(s__ChineseLanguage,s__AssignmentFn__m,'%1(%*{2-}[,])')

chinese_format.kif 346-346
s__format(s__EnglishLanguage,s__AssignmentFn__m,'%1(%*{2-}[,])')

english_format.kif 207-207
s__format(s__FrenchLanguage,s__AssignmentFn__m,'%1(%*{2-}[,])')

french_format.kif 197-197
s__format(s__ItalianLanguage,s__AssignmentFn__m,'%1(%*{2-}[,]')

relations-it.txt 28-28
s__format(s__PortugueseLanguage,s__AssignmentFn__m,'%1(%*{2-}[,])')

portuguese_format.kif 149-149
s__format(s__ar__m,s__AssignmentFn__m,'%1 (%*{2-}[])')

arabic_format.kif 140-140
s__format(s__cz__m,s__AssignmentFn__m,'%1(%*{2-}[,])')

relations-cz.txt 205-205
s__format(s__de__m,s__AssignmentFn__m,'%1(%*{2-}[,])')

relations-de.txt 462-462
s__format(s__hi__m,s__AssignmentFn__m,'%1(%*{2-}[,]')

relations-hindi.txt 72-72
s__format(s__tg__m,s__AssignmentFn__m,'%1(%*{2-}[,]')

relations-cb.txt 62-62
s__termFormat(s__ChineseLanguage,s__AssignmentFn__m,'分派函数')

chinese_format.kif 347-347 "分派函数" is the printable form of assignment in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__AssignmentFn__m,'assignment')

domainEnglishFormat.kif 1894-1894 "assignment" is the printable form of assignment in english language
s__termFormat(s__ar__m,s__AssignmentFn__m,'«لقاء»')

arabic_format.kif 590-590 "«لقاء»" is the printable form of assignment in ar
s__termFormat(s__tg__m,s__AssignmentFn__m,'tungkulin ng takdan')

relations-tg.txt 73-73 "tungkulin ng takdan" is the printable form of assignment in tg

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


( ! [V__FUNCTION,V__CLASS,V__ROW1,V__VALUE] :
   ((s__range(V__FUNCTION,V__CLASS)
     &
     (s__AssignmentFn_2(V__FUNCTION,V__ROW1)
     = V__VALUE))
=>
s__instance(V__VALUE,V__CLASS))
)

Merge.kif 346-350
  • If the range of ?FUNCTION is an instance of ?CLASS and ?FUNCTION(@ROW) is equal to ?VALUE,
  • then ?VALUE is an instance of ?CLASS
( ! [V__FUNCTION,V__CLASS,V__ROW1,V__VALUE] :
   ((s__rangeSubclass(V__FUNCTION,V__CLASS)
     &
     (s__AssignmentFn_2(V__FUNCTION,V__ROW1)
     = V__VALUE))
=>
s__subclass(V__VALUE,V__CLASS))
)

Merge.kif 375-379
  • If the values returned by ?FUNCTION are subclasses of ?CLASS and ?FUNCTION(@ROW) is equal to ?VALUE,
  • then ?VALUE is a subclass of ?CLASS

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


( ! [V__FUNCTION,V__ID,V__CLASS] :
   (s__identityElement(V__FUNCTION,V__ID)
   =>
   (! [V__INST] :
     ((s__domain(V__FUNCTION,1,V__CLASS)
       &
       s__instance(V__INST,V__CLASS))
   =>
   (s__AssignmentFn_3(V__FUNCTION,V__ID,V__INST)
   = V__INST))))
)

Merge.kif 5342-5349
  • If ?ID is an identity element of ?FUNCTION,
  • then for all ?INST
    • if the number 1 argument of ?FUNCTION is an instance of ?CLASS and ?INST is an instance of ?CLASS,
    • then ?FUNCTION(?ID and ?INST) is equal to ?INST
( ! [V__FUN,V__CLASS] :
   (s__instance(V__FUN,s__OneToOneFunction) =>
     (! [V__ARG1,V__ARG2] :
       ((s__domain(V__FUN,1,V__CLASS)
         &
         s__instance(V__ARG1,V__CLASS)
       &
       s__instance(V__ARG2,V__CLASS)
     &
     (~ (V__ARG1 = V__ARG2)))
   =>
   (~ (s__AssignmentFn_2(V__FUN,V__ARG1)
     = s__AssignmentFn_2(V__FUN,V__ARG2))))))
)

Merge.kif 3442-3451
( ! [V__FUNCTION,V__CLASS] :
   (s__instance(V__FUNCTION,s__AssociativeFunction) =>
     (! [V__INST1,V__INST2,V__INST3] :
       ((s__domain(V__FUNCTION,1,V__CLASS)
         &
         s__instance(V__INST1,V__CLASS)
       &
       s__instance(V__INST2,V__CLASS)
     &
     s__instance(V__INST3,V__CLASS))
=>
(s__AssignmentFn_3(V__FUNCTION,V__INST1,s__AssignmentFn_3(V__FUNCTION,V__INST2,V__INST3))
= s__AssignmentFn_3(V__FUNCTION,s__AssignmentFn_3(V__FUNCTION,V__INST1,V__INST2)
,V__INST3)))))
)

Merge.kif 3488-3498
  • If ?FUNCTION is an instance of associative function,
  • then for all ?INST1, ?INST2 and ?INST3
    • if the number 1 argument of ?FUNCTION is an instance of ?CLASS and ?INST1 is an instance of ?CLASS and ?INST2 is an instance of ?CLASS and ?INST3 is an instance of ?CLASS,
    • then ?FUNCTION(?INST1 and ?FUNCTION(?INST2 and ?INST3)) is equal to ?FUNCTION(?FUNCTION(?INST1 and ?INST2) and ?INST3)
( ! [V__FUNCTION,V__CLASS] :
   (s__instance(V__FUNCTION,s__CommutativeFunction) =>
     (! [V__INST1,V__INST2] :
       ((s__domain(V__FUNCTION,1,V__CLASS)
         &
         s__instance(V__INST1,V__CLASS)
       &
       s__instance(V__INST2,V__CLASS))
   =>
   (s__AssignmentFn_3(V__FUNCTION,V__INST1,V__INST2)
   = s__AssignmentFn_3(V__FUNCTION,V__INST2,V__INST1)))))
)

Merge.kif 3510-3519
  • If ?FUNCTION is an instance of commutative function,
  • then for all ?INST1 and ?INST2
    • if the number 1 argument of ?FUNCTION is an instance of ?CLASS and ?INST1 is an instance of ?CLASS and ?INST2 is an instance of ?CLASS,
    • then ?FUNCTION(?INST1 and ?INST2) is equal to ?FUNCTION(?INST2 and ?INST1)


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