SpatioTemporalRegionPartOf

;; Comment: A binary formal between spatio temporal regions.

Defined formal relations between spatiotemporal parts

SpatioTemporalRegionDifference

Definition

(iff (SpatioTemporalRegionPartOf x y) (and ( OccurrentPartOf x y) (SpatioTemporalRegion x) (SpatioTemporalRegion y) ) )

Axioms

Arity

(not (SpatioTemporalRegionPartOf ())
(forall (x) (not SpatioTemporalRegionPartOf x) )
(forall (x y z ...s) (not (SpatioTemporalRegionPartOf x y z ...s) )

Other

(forall ((x SpatioTemporalRegion) (y SpatioTemporalRegion)) (if (not (SpatioTemporalRegionPart x y) ) (exists (z) (SpatioTemporalRegionDifference x y z) ) )
Difference

(forall ((x SpatioTemporalRegion) (y SpatioTemporalRegion)) (exists (z) (SpatioTemporalRegionSumme x y z) ) )
Summe