Object Property: 'part of continuant at all times'

'BFO OWL specification label' "c-part-of_at" ()
'BFO CLIF specification label' "continuantPartOfAt" ()
'example of usage' "Mary’s arm continuant_part_of Mary in the time of her life prior to her operation" (en)
'example of usage' "the Northern hemisphere of the planet Earth is a part of the planet Earth at all times at which the planet Earth exists." (en)
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' "Alan Ruttenberg: This is a binary version of a ternary time-indexed, instance-level, 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)'." ()
'editor note' "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: [028-001])" (en)
'editor note' "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." (en)
'editor note' "BFO2 Reference: continuant" ()
'editor note' "BFO2 Reference: continuantThe range for ‘t’ (as in all cases throughout this document unless otherwise specified) is: temporal region." ()
'editor note' "[copied from inverse property 'has continuant part at all times that part exists'] This is a binary version of a ternary time-indexed, 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'" ()
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: [002-001])" (en)
'has associated axiom(nl)' "continuant_part_of is antisymmetric. (axiom label in BFO2 Reference: [120-001])" (en)
'has associated axiom(nl)' "continuant_part_of is reflexive (every continuant entity is a continuant_part_of itself). (axiom label in BFO2 Reference: [111-002])" (en)
'has associated axiom(nl)' "continuant_part_of is transitive. (axiom label in BFO2 Reference: [110-001])" (en)
'has associated axiom(nl)' "continuant_part_of satisfies unique product. (axiom label in BFO2 Reference: [122-001])" (en)
'has associated axiom(nl)' "continuant_part_of satisfies weak supplementation. (axiom label in BFO2 Reference: [121-001])" (en)
'has associated axiom(nl)' "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: [047-002])" (en)
'has associated axiom(fol)' "(forall (x t) (if (Continuant x) (continuantPartOfAt x x t))) // axiom label in BFO2 CLIF: [111-002] " ()
'has associated axiom(fol)' "(forall (x y t) (if (and (continuantPartOfAt x y t) (IndependentContinuant x)) (locatedInAt x y t))) // axiom label in BFO2 CLIF: [047-002] " ()
'has associated axiom(fol)' "(forall (x y t) (if (and (continuantPartOfAt x y t) (continuantPartOfAt y x t)) (= x y))) // axiom label in BFO2 CLIF: [120-001] " ()
'has associated axiom(fol)' "(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: [121-001] " ()
'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: [122-001] " ()
'has associated axiom(fol)' "(forall (x y z t) (if (and (continuantPartOfAt x y t) (continuantPartOfAt y z t)) (continuantPartOfAt x z t))) // axiom label in BFO2 CLIF: [110-001] " ()
'has associated axiom(fol)' "(iff (ImmaterialEntity a) (and (IndependentContinuant a) (not (exists (b t) (and (MaterialEntity b) (continuantPartOfAt b a t)))))) // axiom label in BFO2 CLIF: [028-001] " ()
isDefinedBy http://purl.obolibrary.org/obo/bfo.owl
label "part of continuant at all times" (en)

Transitive ('part of continuant at all times')

'has continuant part at all times that part exists'

'part of continuant at some time'

ObjectProperty: 'part of continuant at all times'
'proper part of continuant at all times' ⊆ 'part of continuant at all times'
'member part of at all times' ⊆ 'part of continuant at all times'
'part of continuant at all times' ⊆ 'part of continuant at some time'
'has continuant part at all times that part exists' inverse 'part of continuant at all times''has axiom label' http://purl.obolibrary.org/obo/bfo/axiom/0000601

Object Property: 'part of continuant at all times'

http://purl.obolibrary.org/obo/BFO_0000177

Annotations (27)

Property Characteristics (1)

Inverses (1)

Superproperties (1)

Usage (5)