Variation of Complex Activities

Variation of Complex Activities

Extension Name: 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: subtree.def

Grammar: variation.bnf

Definitions

Definition 1 Two minimal activity trees for ?a are isomorphic iff they can each be embedded into the other as a subtree. 
(forall (?occ1 ?occ2 ?a) (iff (min_equiv ?occ1 ?occ2 ?a)
(and    (subtree_embed ?occ1 ?occ2 ?a)
        (subtree_embed ?occ2 ?occ1 ?a))))
Definition 2 An activity is uniform iff all of its minimal activity trees are isomorphic. 
(forall (?a) (iff (uniform ?a)
(forall (?occ1 ?occ2)
        (if	  (and    (root ?occ1 ?a)
                          (root ?occ2 ?a))
                  (min_equiv ?occ1 ?occ2 ?a)))))
Definition 3 An activity ?a is variegated iff all of its minimal activity trees whose root occurrences are occurrence-equivalent are also isomorphic. 
(forall (?a) (iff (variegated ?a)
(and    (exists (?a1)
                (forall (?occ1 ?occ2)
                        (if	  (and    (occurrence_of ?occ1 ?a1)
                                          (occurrence_of ?occ2 ?a1)
					  (root ?occ1 ?a)
					  (root ?occ2 ?a))
                                  (min_equiv ?occ1 ?occ2 ?a))))
        (exists (?a2 ?occ3 ?occ4)
                (and    (occurrence_of ?occ3 ?a2)
                        (occurrence_of ?occ4 ?a2)
			(root ?occ3 ?a)
			(root ?occ4 ?a)
                        (not (min_equiv ?occ3 ?occ4 ?a)))))))
Definition 4 An activity is multiform iff there exist nonisomorphic activity trees whose root occurrences are occurrence equivalent. 
(forall (?a) (iff (multiform ?a)
(forall (?a1 ?occ1)
	(if	  (and	(root ?occ1 ?a)
			(occurrence_of ?occ1 ?a1))
        	  (exists (?occ2 ?occ3)
                	(and    (occurrence_of ?occ2 ?a1)
                        	(occurrence_of ?occ3 ?a1)
				(root ?occ2 ?a)
				(root ?occ3 ?a)
                        	(not (min_equiv ?occ2 ?occ3 ?a))))))))