Attributes  Values 

Type
 
subPropertyOf
 
example of usage
  Mary’s arm continuant_part_of Mary in the time of her life prior to her operation
 the Northern hemisphere of the planet Earth is a part of the planet Earth at all times at which the planet Earth exists.

definition
  [copied from inverse property 'has continuant part at all times that part exists'] forall(t) exists_at(y,t) > exists_at(x,t) and 'has continuant part'(x,y,t)

editor note
  BFO2 Reference: continuantThe range for ‘t’ (as in all cases throughout this document unless otherwise specified) is: temporal region.
 BFO 2 Reference: Immaterial entities are in some cases continuant parts of their material hosts. Thus the hold of a ship, for example, is a part of the ship; it may itself have parts, which may have names (used for example by ship stow planners, customs inspectors, and the like). Immaterial entities under both 1. and 2. can be of zero, one, two or three dimensions. We define:a(immaterial entity)[Definition: a is an immaterial entity = Def. a is an independent continuant that has no material entities as parts. (axiom label in BFO2 Reference: [028001])
 BFO2 Reference: continuant
 [copied from inverse property 'has continuant part at all times that part exists'] This is a binary version of a ternary timeindexed, instance level, relation. Unlike the rest of the temporalized relations which temporally quantify over existence of the subject of the relation, this relation temporally quantifies over the existence of the object of the relation. The relation is provided tentatively, to assess whether the GO needs such a relation. It is inverse of 'part of continuant at all times'
 BFO 2 Reference: a (continuant or occurrent) part of itself. We appreciate that this is counterintuitive for some users, since it implies for example that President Obama is a part of himself. However it brings benefits in simplifying the logical formalism, and it captures an important feature of identity, namely that it is the limit case of mereological inclusion.
 Alan Ruttenberg: This is a binary version of a ternary timeindexed, instancelevel, relation. The BFO reading of the binary relation 'part of continuant at all times@en' is: forall(t) exists_at(x,t) > exists_at(y,t) and 'part of continuant@en(x,y,t)'.

imported from
 
elucidation
  b continuant_part_of c at t =Def. b is a part of c at t & t is a time & b and c are continuants. (axiom label in BFO2 Reference: [002001])

has associated axiom(nl)
  continuant_part_of is transitive. (axiom label in BFO2 Reference: [110001])
 continuant_part_of is antisymmetric. (axiom label in BFO2 Reference: [120001])
 continuant_part_of satisfies unique product. (axiom label in BFO2 Reference: [122001])
 continuant_part_of satisfies weak supplementation. (axiom label in BFO2 Reference: [121001])
 continuant_part_of is reflexive (every continuant entity is a continuant_part_of itself). (axiom label in BFO2 Reference: [111002])
 if b continuant_part_of c at t and b is an independent continuant, then b is located_in c at t. (axiom label in BFO2 Reference: [047002])

has associated axiom(fol)
  (forall (x y t) (if (exists (v) (and (continuantPartOfAt v x t) (continuantPartOfAt v y t))) (exists (z) (forall (u w) (iff (iff (continuantPartOfAt w u t) (and (continuantPartOfAt w x t) (continuantPartOfAt w y t))) (= z u)))))) // axiom label in BFO2 CLIF: [122001]
 (iff (ImmaterialEntity a) (and (IndependentContinuant a) (not (exists (b t) (and (MaterialEntity b) (continuantPartOfAt b a t)))))) // axiom label in BFO2 CLIF: [028001]
 (forall (x y t) (if (and (continuantPartOfAt x y t) (not (= x y))) (exists (z) (and (continuantPartOfAt z y t) (not (exists (w) (and (continuantPartOfAt w x t) (continuantPartOfAt w z t)))))))) // axiom label in BFO2 CLIF: [121001]
 (forall (x t) (if (Continuant x) (continuantPartOfAt x x t))) // axiom label in BFO2 CLIF: [111002]
 (forall (x y t) (if (and (continuantPartOfAt x y t) (continuantPartOfAt y x t)) (= x y))) // axiom label in BFO2 CLIF: [120001]
 (forall (x y z t) (if (and (continuantPartOfAt x y t) (continuantPartOfAt y z t)) (continuantPartOfAt x z t))) // axiom label in BFO2 CLIF: [110001]
 (forall (x y t) (if (and (continuantPartOfAt x y t) (IndependentContinuant x)) (locatedInAt x y t))) // axiom label in BFO2 CLIF: [047002]

BFO OWL specification label
 
BFO CLIF specification label
 
label
  continuant part of at all times
 part of continuant at all times

domain
 
range
 
isDefinedBy
 
preferred label
  continuant part of at all times

described by
 
Identifier
 
definition
  b continuant part of c at all times =Def for all times t, (b exists at t, implies b continuant part of c at t & t is a temporal region & b and c are continuants)

example
  Centre of mass of a material entity continuant part of material entity at all times; continuant fiat external boundary of an object continuant part of object at all times.

is subPropertyOf
of  
is inverseOf
of  
is annotatedSource
of  
is annotatedTarget
of  
is onProperty
of  
is topic
of  