mereological product fn (MereologicalProductFn)

(MereologicalProductFn obj1 obj2) denotes the Object consisting of the parts which belong to both obj1 and 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 product 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 difference 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 MereologicalProductFn(objekt, objekt)

Axiomy (4)

mereological sum fn je internally related to mereological product fn.

(relatedInternalConcept MereologicalSumFn MereologicalProductFn)

mereological product fn je internally related to mereological difference fn.

(relatedInternalConcept MereologicalProductFn MereologicalDifferenceFn)

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

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

Jestliže hole je díra v obj1 a hole je díra v obj2, potom existuje obj3 tak, že obj3 je vlastní částí "mereological product fn(obj1,obj2)" a hole je díra v obj3.

(=>
      (and
            (hole ?HOLE ?OBJ1)
            (hole ?HOLE ?OBJ2))
      (exists
            (?OBJ3)
            (and
                  (properPart
                        ?OBJ3
                        (MereologicalProductFn ?OBJ1 ?OBJ2))
                  (hole ?HOLE ?OBJ3))))