SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > BinaryRelation > AntisymmetricRelation > AsymmetricRelation > properPart
Next AsymmetricRelationproperty    UpAsymmetricRelation, TransitiveRelation    Previous AsymmetricRelationproperlyFills   

properPart
subjectfact 
properPartdocumentation (properPart ?OBJ1 ?OBJ2) means that ?OBJ1 is a part of ?OBJ2 other than ?OBJ2 itself. This is a TransitiveRelation and AsymmetricRelation (hence an IrreflexiveRelation)2001-11-30 13:35:04.0
has axiom
(<=> 
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
2001-11-30 13:35:04.0
has axiom
(=> 
(and
(fills ?OBJ ?HOLE1)
(properPart ?HOLE2 ?HOLE1))
(completelyFills ?OBJ ?HOLE2))
2001-11-30 13:35:04.0
has axiom
(=> 
(and
(fills ?OBJ1 ?HOLE)
(properPart ?OBJ2 ?OBJ1))
(properlyFills ?OBJ2 ?HOLE))
2001-11-30 13:35:04.0
has axiom
(=> 
(and
(hole ?HOLE ?OBJ1)
(hole ?HOLE ?OBJ2))
(exists (?OBJ3)
(and
(properPart ?OBJ3 (MereologicalProductFn ?OBJ1 ?OBJ2))
(hole ?HOLE ?OBJ3))))
2001-11-30 13:35:04.0
has axiom
(=> 
(and
(instance ?HOLE1 Hole)
(properPart ?HOLE2 ?HOLE1))
(exists (?OBJ)
(and
(meetsSpatially ?HOLE1 ?OBJ)
(not
(meetsSpatially ?HOLE2 ?OBJ)))))
2001-11-30 13:35:05.0
has axiom
(=> 
(instance ?HOLE1 Hole)
(exists (?HOLE2)
(properPart ?HOLE2 ?HOLE1)))
2001-11-30 13:35:05.0
is an instance of AsymmetricRelation2001-11-30 13:35:05.0
is an instance of TransitiveRelation2001-11-30 13:35:05.0
BinaryRelationis first domain of DomainFn2001-11-30 13:33:44.0
is first domain of equivalenceRelationOn2001-11-30 13:33:44.0
is first domain of inverse2001-11-30 13:33:44.0
is first domain of irreflexiveOn2001-11-30 13:33:44.0
is first domain of partialOrderingOn2001-11-30 13:33:44.0
is first domain of RangeFn2001-11-30 13:33:44.0
is first domain of reflexiveOn2001-11-30 13:33:44.0
is first domain of totalOrderingOn2001-11-30 13:33:44.0
is first domain of trichotomizingOn2001-11-30 13:33:44.0
is second domain of inverse2001-11-30 13:33:44.0
Classis third domain of domain2001-11-30 13:33:51.0
is third domain of domainSubclass2001-11-30 13:33:51.0
Abstractis disjoint from Physical2001-11-30 13:33:32.0

Next AsymmetricRelationproperty    UpAsymmetricRelation, TransitiveRelation    Previous AsymmetricRelationproperlyFills