Duration Constraints on Embedded Activity Occurrences

Ordering and Duration Constraints on Embedded Activity Occurrences

Extension Name: embed_dur.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

Definitional Extensions Required by this Extension: permute.def

Grammar: embed_dur.bnf

Definitions

Definition 1 An activity is embed duration if and only if all branch automorphic occurences in the same tree have the same duration. 
(forall (?a) (iff (embed_duration ?a) 
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(same_grove ?occ1 ?occ2)
			(branch_automorphic ?occ1 ?occ2))
		  (duration_equiv ?occ1 ?occ2)))))
Definition 2 An activity is a partial embed duration activity if and only if there exist occurrences such that all branch automorphic occurrences in the same tree have the same duration. 
(forall (?a) (iff (partial_embed_duration ?a) 
(and    (exists (?occ1)
                (forall (?occ2)
                        (if	  (and  (occurrence_of ?occ1 ?a)
                                        (occurrence_of ?occ2 ?a)
					(same_grove ?occ1 ?occ2)
					(branch_automorphic ?occ1 ?occ2))
                                  (dur_equiv ?occ1 ?occ2))))
        (exists (?occ3 ?occ4)
                (and    (occurrence_of ?occ3 ?a)
                        (occurrence_of ?occ4 ?a)
			(same_grove ?occ3 ?occ4)
                        (branch_automorphic ?occ3 ?occ4)
                        (not (dur_equiv ?occ3 ?occ4)))))))
Definition 3 An activity is nonembed duration if and only if for any occurrence there exist branch automorphic occurrences of the activity in the same tree that have unequal durations. 
(forall (?a) (iff (nonembed_duration ?a) 
(exists (?occ1 ?occ2)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(same_grove ?occ1 ?occ2)
		(branch_automorphic ?occ1 ?occ2)
		(not (duration_equiv ?occ1 ?occ2))))))