Ordering and Duration Constraints on Activity Occurrences

Ordering and Duration Constraints on Activity Occurrences

Extension Name: ordered_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: ordered_dur.bnf

Definitions

Definition 1 An activity is ordered duration if and only if all branch automorphic occurences have the same duration. 
(forall (?a) (iff (ordered_duration ?a) 
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(branch_automorphic ?occ1 ?occ2))
		  (duration_equiv ?occ1 ?occ2)))))
Definition 2 An activity is a context duration activity if and only if there exist occurrences such that all branch automorphic occurrences have the same duration. 
(forall (?a) (iff (partial_ordered_duration ?a) 
(and    (exists (?occ1)
                (forall (?occ2)
                        (if	  (and  (occurrence_of ?occ1 ?a)
                                        (occurrence_of ?occ2 ?a)
					(branch_automorphic ?occ1 ?occ2))
                                  (dur_equiv ?occ1 ?occ2))))
        (exists (?occ3 ?occ4)
                (and    (occurrence_of ?occ3 ?a)
                        (occurrence_of ?occ4 ?a)
                        (branch_automorphic ?occ3 ?occ4)
                        (not (dur_equiv ?occ3 ?occ4)))))))
Definition 3 An activity is unordered duration if and only if for any occurrence there exist branch automorphic occurrences of the activity that have unequal durations. 
(forall (?a) (iff (unordered_duration ?a) 
(exists (?occ1 ?occ2)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(branch_automorphic ?occ1 ?occ2)
		(not (duration_equiv ?occ1 ?occ2))))))