分配 (distributes)

A BinaryFunction function1 is distributive over another BinaryFunction function2 just in case (function1 inst1 (function2 inst2 inst3)) is equal to (function2 (function1 inst1 inst2) (function1 inst1 inst3)), for all inst1, inst2, and inst3.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

種類

可繼承關係

二元述詞

種類

可繼承關係

二元關係

分配

Coordinate term(s)

弧線重量作者先於或同時肇因次類肇因公民封閉於相連的包含訊息共生複製日期降低可能性發展期形式無交集文字說明持續時間較早編者元素雇用相等等同關係於利用以...語言表達面對家族關係完成次數圖部分大於大於或等於有意圖有技巧在...期間為真須使...為真有權使...為真洞同一元素串列中在注意範圍中增加可能性獨立或然率居住抑制初始化序列實例倒序非反射於... 大於小於小於或等於物質測量時段相接情態屬性時段重疊雙親偏序於... 部分位於路徑長擁有先決條件避免特性出版範圍範圍次種類提及反射於... SUMO內部相關概念兄弟姊妹小於開始次屬性次聚集次圖次序列次歷程次命題次種類次關係包含訊息種類包含訊息實例續接屬性封閉續接屬性時間部分時間全序於... 三分法使用（結合）價人造物版本

Type restrictions

distributes(二元函數, 二元函數)

Axioms (1)

if 分配(function1,function2) holds,
then for all inst1,inst2,inst3 holds: if function1 的論元是 class1 的實例 and inst1 是 class1 的實例 and inst2 是 class1 的實例 and inst3 是 class1 的實例 and function2 的論元是 class2 的實例 and inst1 是 class2 的實例 and inst2 是 class2 的實例 and inst3 是 class2 的實例, then "function1(inst1,"function2(inst2,inst3)")" 等於 "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))