Distribution of Complex Activities

Distribution of Complex Activities

Extension Name: 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: none

Grammar: distribution.bnf

Definitions

Definition 1 The activity occurrence ?occ is an element of the profile for the activity ?a iff ?occ is the initial occurrence in a branch of the occurrence tree that is occurrence-isomorphic to a branch of an activity tree for ?a. 
(forall (?occ ?a) (iff (profile ?occ ?a)
(exists (?occ1 ?occ2 ?a1)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ ?a1)
		(occurrence_of ?occ2 ?a1)
		(= ?occ2 (root_occ ?occ1))
		(forall (?occ3 ?a2)
			(if	  (and	(subactivity_occurrence ?occ3 ?occ1)
					(occurrence_of ?occ3 ?a2))
				  (exists (?occ4)
					(and	(occurrence_of ?occ4 ?a2)
						(precedes ?occ ?occ4)))))))))
Definition 2 Two activity occurrences ?occ1 and ?occ2 in the occurrence tree are root-equivalent with respect to an activity ?a if and only if there exist occurrences of ?a succeeding both ?occ1 and ?occ2. 
(forall (?a ?occ1 ?occ2) (iff (root_equiv ?a ?occ1 ?occ2)
(if	  (and	(profile ?occ1 ?a)
		(profile ?occ2 ?a))
	  (iff	(root ?occ1 ?a)
		(root ?occ2 ?a)))))
Definition 3 An activity is universal iff it occurs whenever it is possible. 
(forall (?a) (iff (universal ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(profile ?occ1 ?a)
			(profile ?occ2 ?a))
		  (root_equiv ?a ?occ1 ?occ2)))))
Definition 4 An activity is restricted iff there exist activities that are root equivalent. 
(forall (?a) (iff (restricted ?a)
(and    (exists (?a1)
                (forall (?occ1 ?occ2)
                        (if	  (and    (occurrence_of ?occ1 ?a1)
                                          (occurrence_of ?occ2 ?a1)
					  (profile ?occ1 ?a)
					  (profile ?occ2 ?a))
                                  (root_equiv ?a ?occ1 ?occ2))))
        (exists (?a2 ?occ3 ?occ4)
                (and    (occurrence_of ?occ3 ?a2)
                        (occurrence_of ?occ4 ?a2)
			(profile ?occ3 ?a)
			(profile ?occ4 ?a)
                        (not (root_equiv ?a ?occ3 ?occ4)))))))
Definition 5 An activity is constrained iff every activity has occurrences that are not root equivalent. 
(forall (?a) (iff (local ?a)
(forall (?a1)
        (exists (?occ1 ?occ2)
                (and    (occurrence_of ?occ1 ?a1)
                        (occurrence_of ?occ2 ?a1)
			(profile ?occ1 ?a)
			(profile ?occ2 ?a)
                        (not (root_equiv ?a ?occ1 ?occ2)))))))