Activity Trees and Reordering

Activity Trees and Reordering

Extension Name: treeordered.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: ordered.def

Grammar: treeordered.bnf

Definitions

Definition 1 An activity is treeordered iff the root subactivity occurrence of one occurrence is root automorphic with every other root subactivity occurrence of other occurrences of the activity. 
(forall (?a) (iff (treeordered ?a)
(forall (?occ1 ?occ2)
        (if	  (and  (occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (same_grove ?occ1 ?occ2)))
                  (root_automorphic ?occ1 ?occ2)))))
Definition 2 An activity occurrence is nondeterministically treeordered iff each root subactivity occurrence of the minimal activity tree is root automorphic to some other root subactivity occurrence in the occurrence tree. 
(forall (?a) (iff (nondet_treeordered ?a)
(forall (?occ1)
        (if	  (occurrence_of ?occ1 ?a)
                  (exists (?occ2)
                        (and    (occurence_of ?occ2 ?a)
                                (not (same_grove ?occ1 ?occ2))
                                (root_automorphic ?occ1 ?occ2)))))))
Definition 3 An activity is partially treeordered iff there exist root subactivity occurrences of the minimal activity tree that are root automorphic to some other root subactivity occurrences in the occurrence tree, and there also exist root subactivity occurrences that are not root automorphic to any other root subactivity occurrence. 
(forall (?a) (iff (partial_treeordered ?a)
(exists (?occ1 ?occ2)
        (and    (occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
                (not (same_grove ?occ1 ?occ2))
                (root_automorphic ?occ1 ?occ2)
                (forall (?occ3)
                        (if	  (and  (occurrence_of ?occ3 ?a)
                                        (not (same_grove ?occ3 ?occ2)))
                                  (not (root_automorphic ?occ3 ?occ2))))))))
Definition 4 An activity is scrambled iff none of the branches in an activity tree are root automorphic to any other activity tree. 
(forall (?a) (iff (scrambled ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (same_grove ?occ1 ?occ2)))
		  (not (root_automorphic ?occ1 ?occ2))))))