Time-based Variation of Complex Activities

Time-based Variation of Complex Activities

Extension Name: time_variation.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

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

Grammar: time_variation.bnf

Definitions

Definition 1 A complex activity is time conditional iff any two of its minimal activity trees are isomorphic iff the roots agree on their beginof timepoints. 
(forall (?a) (iff (time_conditional ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2))
		  (min_equiv ?occ1 ?occ2 ?a)))))
Definition 2 A complex activity is partial time conditional if and only if there exist occurrence-preserving automorphisms. 
(forall (?a) (iff (partial_time_conditional ?a)
(and	(exists (?occ1)
		(forall (?occ2)
			(if	  (and	(root ?occ1 ?a)
					(root ?occ2 ?a)
					(begin_equiv ?occ1 ?occ2))
				  (min_equiv ?occ1 ?occ2 ?a))))
	(exists (?occ3 ?occ4)
		(and	(root ?occ3 ?a)
			(root ?occ4 ?a)
			(begin_equiv ?occ3 ?occ4)
			(not (min_equiv ?occ3 ?occ4 ?a)))))))
Definition 3 A complex activity is rigid time conditional if and only if the only occurrence-preserving timeline automorphism is the trivial one. 
(forall (?a) (iff (rigid_time_conditional ?a)
(forall (?occ1)
	(exists (?occ2)
		(and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2)
			(not (min_equiv ?occ1 ?occ2 ?a)))))))