OccurrentPartOf

;; Comment: A binary formal between occurrents.

Defined formal relations

SpatioTemporalRegionPartOf

Axioms

Domain and range

(forall (x y) (if (OccurrentPartOf x y) (Occurrent x) )

(forall (x y) (if (OccurrentPartOf x y) (Occurrent y) )

Arity

(not (OccurrentPartOf ())
(forall (x) (not (OccurrentPartOf x) )
(forall (x y z ...s) (not (OccurrentPartOfx y z ...s) )

Other

(forall ((x Occurrent)) (OccurrentPartOf x x))
Reflexivity

(forall ((x Occurrent) (y Occurrent)) (if (and (OccurrentPartOf x y) (OccurrentPartOf y x) ) (x =y) )
Antisymmetry

(forall ((x Occurrent) (y Occurrent) (z Occurrent)) (if (and (OccurrentPartOf x y) (OccurrentPartOf y z) ) (OccurrentPartOf x z) )
Transitivity

(forall (x y) (if (OccurrentPartOf x y) ( iff (ProcessualEntity x) (ProcessualEntity y) ) )
Only processural entities are parts of processual entities.

(forall (x y) (if (OccurrentPartOf x y) ( iff (SpatioTemporalRegion x) (SpatioTemporalRegion y) ) )
Only spatio temporal regions are parts of spatio temporal regions

(forall (x y) (if (OccurrentPartOf x y) ( iff ( TemporalRegion x) ( TemporalRegion y) ) )
Only] temporal regions are parts of regions