mereological difference fn (MereologicalDifferenceFn)

(MereologicalDifferenceFn obj1 obj2) denotes the Object consisting of the parts which belong to obj1 and not to obj2.

Ontologie

SUMO / MEREOTOPOLOGY

Class(es)

třída

inheritable relation

prostorová relace
is instance of

třída

inheritable relation

binární funkce
is instance of

mereological difference fn

Související termín(y)

addition fn back fn day fn density fn division fn edition fn exponentiation fn front fn graph path fn hour fn intersection fn interval fn kappa fn list concatenate fn list order fn log fn max fn maximal weighted path fn measure fn mereological product fn mereological sum fn min fn minimal weighted path fn minute fn month fn multiplication fn periodical issue fn principal host fn recurrent time interval fn relative complement fn relative time fn remainder fn second fn series volume fn skin fn speed fn subtraction fn temporal composition fn time interval fn union fn where fn between connected connects distance hole larger orientation part partially fills partly located smaller traverses

Typy argumentů

objekt MereologicalDifferenceFn(objekt, objekt)

Axiomy (3)

mereological sum fn je internally related to mereological difference fn.

(relatedInternalConcept MereologicalSumFn MereologicalDifferenceFn)

mereological product fn je internally related to mereological difference fn.

(relatedInternalConcept MereologicalProductFn MereologicalDifferenceFn)

Jestliže obj3 se rovná "mereological difference fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part není částí obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (not
                              (part ?PART ?OBJ2))))))