Temporal Distribution of Complex Activities

Temporal Distribution of Complex Activities

Extension Name: time_distribution.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: act_occ.th, disc_state.th, complex.th, atomic.th, subactivity.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: distribution.def, start.def

Grammar: time_distribution.bnf

Definitions

Definition 1 An activity is a launch activity if and only if whenever two occurrences agree on their beginof timepoints, then they agree on the occurrences of the activity. 
 
(forall (?a) (iff (launch ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(profile ?occ1 ?a)
			(profile ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2))
		  (root_equiv ?a ?occ1 ?occ2)))))
Definition 2 An activity is a partial launch activity if and only if there exist occurrences that agree on their beginof timepoints and on the occurrence of the activity. 
 
(forall (?a) (iff (partial_launch ?a)
(and    (exists (?occ1)
                (forall (?occ2)
                        (if	  (and	(profile ?occ1 ?a)
					(profile ?occ2 ?a)
					(begin_equiv ?occ1 ?occ2))
                                  (root_equiv ?a ?occ1 ?occ2))))
        (exists (?occ3 ?occ4)
                (and    (profile ?occ3 ?a)
			(profile ?occ4 ?a)
			(begin_equiv ?occ3 ?occ4)
                        (not (root_equiv ?a ?occ3 ?occ4)))))))
Definition 3 An activity is a rigid launch activity if and only if the only occurrence-preserving timeline automorphism is the trivial one. 
 
(forall (?a) (iff (rigid_launch ?a)
(forall (?occ1)
	(if	  (profile ?occ1 ?a)
        	  (exists (?occ2)
                	(and    (begin_equiv ?occ1 ?occ2)
                        	(not (root_equiv ?a ?occ1 ?occ2))))))))