bu4 fen5 zheng3 ti1 cha4 yi4 han2 shu4 (MereologicalDifferenceFn)
(MereologicalDifferenceFn obj1
obj2) denotes the Object consisting of the parts which belong to obj1
and not to obj2.
Ontology
SUMO / MEREOTOPOLOGYClass(es)
Coordinate term(s)
jia1 fa3 han2 shu4
fan3 mian4 han2 shu4
ri4 han2 shu4
mi4 du4 han2 shu4
chu2 fa3 han2 shu4
wen2 ben3 ban3 ben3 han2 shu4
zhi3 shu4 han2 shu4
zheng4 mian4 han2 shu4
tu2 lu4 jing4 han2 shu4
xiao3 shi2 han2 shu4
jiao1 ji2 han2 shu4
jian1 ge2 han2 shu4
zhong3 lei4 miao2 shu4 han2 shu4
lie4 jie2 han2 shu4
lie4 xu4 han2 shu4
dui4 shu4 han2 shu4
zui4 da4 zhi2 han2 shu4
zui4 da4 liang4 lu4 jing4 han2 shu4
ce4 liang4 han2 shu4
bu4 fen5 zheng3 ti1 jiao1 ji2 han2 shu4
bu4 fen5 zheng3 ti1 jia1 zong1 han2 shu4
zui4 xiao3 zhi2 han2 shu4
zui4 xiao3 liang4 lu4 jing4 han2 shu4
fen1 zhong1 han2 shu4
yue4 fen4 han2 shu4
cheng2 fa3 han2 shu4
qi1 kan1 yi1 qi1 han2 shu4
zhu3 ti1 han2 shu4
zhou1 qi1 xing4 shi2 ju4 han2 shu4
guan1 xi4 hu4 bu3 han2 shu4
xiang4 dui4 shi2 jian1 han2 shu4
yu2 shu4 han2 shu4
miao3 zhong1 han2 shu4
xi4 lie4 yi1 juan4 han2 shu4
biao3 pi2 han2 shu4
su4 du4 han2 shu4
jian3 fa3 han2 shu4
shi2 jian1 dan1 wei4 han2 shu4
shi2 jian1 li4 cheng2 han2 shu4
lian2 ji2 han2 shu4
wei4 zhi4 han2 shu4
jie4 yu1
xiang1 lian2 de5
xiang1 lian2
ju4 li2
dong4
da4 yu1
xiang4 dui4 fang1 wei4
bu4 fen5
bu4 fen5 tian2 chong1
bu4 fen5 wei4 yu1
xiao3 yu1
heng2 yue4
Type restrictions
wu4 ti1 MereologicalDifferenceFn(wu4 ti1, wu4 ti1)
Axioms (3)
bu4 fen5 zheng3 ti1 jia1 zong1 han2 shu4 na4 bu4 xiang1 guan1 yu1 bu4 fen5 zheng3 ti1 cha4 yi4 han2 shu4.
(relatedInternalConcept MereologicalSumFn MereologicalDifferenceFn)
bu4 fen5 zheng3 ti1 jiao1 ji2 han2 shu4 na4 bu4 xiang1 guan1 yu1 bu4 fen5 zheng3 ti1 cha4 yi4 han2 shu4.
(relatedInternalConcept MereologicalProductFn MereologicalDifferenceFn)
If obj3 deng3 yu1 "obj1 he2 obj2 de5 cha4 yi4", then for all part holds: part shi4 obj3 de5 bu4 fen5) if and only if part shi4 obj1 de5 bu4 fen5) and part shi4 obj2 de5 bu4 fen5).
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))