mereological difference fn (MereologicalDifferenceFn)

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

Ontology

SUMO / MEREOTOPOLOGY

Class(es)

Classe

inheritable relation

RelazioneSpaziale
is instance of

Classe

inheritable relation

FunzioneBinaria
is instance of

mereological difference fn

Coordinate term(s)

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

Type restrictions

Oggetto MereologicalDifferenceFn(Oggetto, Oggetto)

Axioms (3)

mereological sum fn é interamente correlato a mereological difference fn.

(relatedInternalConcept MereologicalSumFn MereologicalDifferenceFn)

mereological product fn é interamente correlato a mereological difference fn.

(relatedInternalConcept MereologicalProductFn MereologicalDifferenceFn)

Se obj3 is uguale a "la differenza tra le parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 e part é not una parte di obj2.

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