proper part (properPart)

(properPart obj1 obj2) means that obj1 is a part of obj2 other than obj2 itself. This is a TransitiveRelation and AsymmetricRelation (hence an IrreflexiveRelation).

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

asymmetric relation
is instance of

transitive relation
is instance of

proper part

Superrelation(s)

partly located

located

part

proper part

Subrelation(s)

engineering subcomponent

Coordinate term(s)

back fn cardinality fn front fn principal host fn probability fn skin fn attribute authors before causes causes subclass citizen closed on completely fills contains information crosses date developmental form documentation duration during earlier editor element equivalence relation on exploits expressed in language fills finishes frequency graph part greater than has purpose has skill holds during holds obligation holds right hole identity element immediate instance immediate subclass in list in scope of interest inhabits interior part irreflexive on larger less than manner measure meets temporally member modal attribute parent partial ordering on partially fills path length penetrates possesses precondition properly fills publishes range range subclass realization reflexive on smaller starts sub collection sub graph sub organizations sub plan sub proposition successor attribute successor attribute closure superficial part surface temporal part time total ordering on trichotomizing on uses valence version

Related WordNet synsets

part, portion: something less than the whole of a human artifact: "the rear part of the house"; "glue the two parts together"

See more related synsets on a separate page.

Axioms (8)

obj1 is a properPart of obj2 if and only if obj1 is a part of obj2 and obj2 is not a part of obj1.

(<=>
      (properPart ?OBJ1 ?OBJ2)
      (and
            (part ?OBJ1 ?OBJ2)
            (not
                  (part ?OBJ2 ?OBJ1))))

If hole is a hole in obj1 and hole is a hole in obj2, then there exists obj3 so that obj3 is a properPart of "the intersection of the parts of obj1 and obj2" and hole is a hole in obj3.

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

If hole1 is an instance of hole, then there exists hole2 so that hole2 is a properPart of hole1.

(=>
      (instance ?HOLE1 Hole)
      (exists
            (?HOLE2)
            (properPart ?HOLE2 ?HOLE1)))

If hole1 is an instance of hole and hole2 is a properPart of hole1, then there exists obj so that hole1 meets obj and hole2 doesn't meet obj.

(=>
      (and
            (instance ?HOLE1 Hole)
            (properPart ?HOLE2 ?HOLE1))
      (exists
            (?OBJ)
            (and
                  (meetsSpatially ?HOLE1 ?OBJ)
                  (not
                        (meetsSpatially ?HOLE2 ?OBJ)))))

If obj fills hole1 and hole2 is a properPart of hole1, then obj completely fills hole2.

(=>
      (and
            (fills ?OBJ ?HOLE1)
            (properPart ?HOLE2 ?HOLE1))
      (completelyFills ?OBJ ?HOLE2))

If obj1 fills hole and obj2 is a properPart of obj1, then obj2 properly fills hole.

(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (properPart ?OBJ2 ?OBJ1))
      (properlyFills ?OBJ2 ?HOLE))

If state is an instance of state or province, then there exists nation land so that state is a properPart of land.

(=>
      (instance ?STATE StateOrProvince)
      (exists
            (?LAND)
            (and
                  (instance ?LAND Nation)
                  (properPart ?STATE ?LAND))))

If room is an instance of room, then there exists building build so that room is a properPart of build.

(=>
      (instance ?ROOM Room)
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Building)
                  (properPart ?ROOM ?BUILD))))