Permuting Activity Trees

Permuting Activity Trees

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

Grammar: branchwise.bnf

Definitions

Definition 1 An activity is reordered iff the set of atomic subactivity occurrences on each branch of one minimal activity tree is a permutation of the atomic subactivity occurrences on a branch in another activity tree for ?a. 
(forall (?a) (iff (reordered ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a))
		  (branch_automorphic ?occ1 ?occ2)))))
Definition 2 An activity is nondeterministically reordered iff the set of atomic subactivity occurrences on each branch of one minimal activity tree for ?a is a permutation of the atomic subactivity occurrences on some branch of another minimal activity tree for ?a. 
(forall (?a) (iff (nondet_reordered ?a)
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(not (same_grove ?occ1 ?occ2))
				(branch_automorphic ?occ1 ?occ2)))))))
Definition 3 An activity is partially reordered iff there exists a branch such that the set of atomic subactivity occurrences is a permutation of the atomic subactivity occurrences on some other branch, and there exists a branch that is not a permutation of any other branch. 
(forall (?a) (iff (partial_reordered ?a)
(exists (?occ1 ?occ2 ?occ3)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(not (same_grove ?occ1 ?occ2))
		(branch_automorphic ?occ1 ?occ2)
		(occurrence_of ?occ3 ?a)
		(same_grove ?occ1 ?occ3)
		(forall (?occ4)
			(if	  (and	(occurrence_of ?occ4 ?a)
					(not (= ?occ2 ?occ4))
					(same_grove ?occ2 ?occ4))
				  (not (branch_automorphic ?occ2 ?occ4))))))))
Definition 4 An activity is nonorderable iff none of the branches in an activity tree are branch automorphic to any other branches in other activity trees in the spectrum. 
(forall (?a) (iff (unorderable ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (same_grove ?occ1 ?occ2)))
		  (not (branch_automorphic ?occ1 ?occ2))))))