Mixed Variation of Complex Activities

Mixed Variation of Complex Activities

Extension Name: mixed_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, precond.def, start.def

Grammar: mixed_variation.bnf

Definitions

Definition 1 An activity is mixed conditional if and only if any two of its minimal activity trees are isomorphic if and only if the roots agree on state and the timepoint and which they begin. 
(forall (?a) (iff (mixed_conditional ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2)
			(state_equiv ?occ1 ?occ2))
		  (min_equiv ?occ1 ?occ2 ?a)))))
Definition 2 An activity is partial mixed conditional if and only if there exist minimal activity trees that are isomorphic if and only if the roots agree on state and the timepoint and which they begin. 
(forall (?a) (iff (partial_mixed_conditional ?a)
(and	(exists (?occ1)
		(forall (?occ2)
			(if	  (and	(root ?occ1 ?a)
					(root ?occ2 ?a)
					(begin_equiv ?occ1 ?occ2)
					(state_equiv ?occ1 ?occ2))
				  (min_equiv ?occ1 ?occ2 ?a))))
	(exists (?occ3 ?occ4)
		(and	(root ?occ3 ?a)
			(root ?occ4 ?a)
			(begin_equiv ?occ3 ?occ4)
			(state_equiv ?occ3 ?occ4)
			(not (min_equiv ?occ3 ?occ4 ?a)))))))
Definition 3 An activity is rigid mixed conditional if and only if the only automorphisms that preserve occurrences, timepoints, and state are the trivial ones. 
(forall (?a) (iff (rigid_mixed_conditional ?a)
(forall (?occ1)
	(exists (?occ2)
		(and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2)
			(state_equiv ?occ1 ?occ2)
			(not (min_equiv ?occ1 ?occ2 ?a)))))))