Permuting Branch Structure

Permuting Branch Structure

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

Grammar: permute.bnf

Definitions

Definition 1 One branch of a minimal activity tree is branch-monomorphic to another iff there exists a one-to-one mapping of the set of atomic activity occurrences in the one branch into the set of atomic activity occurrences on the other branch. 
(forall (?occ1 ?occ2) (iff (branch_monomorphic ?occ1 ?occ2)
(forall (?s1 ?a)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(subactivity_occurrence ?s1 ?occ1))
		  (exists (?s2)
			(and	(subactivity_occurrence ?s2 ?occ2)
				(mono ?s1 ?s2 ?a)))))))
Definition 2 Two branches of a minimal activity tree are branch-automorphic iff the set of atomic activity occurrences on one branch is a permutation of the the set of atomic activity occurrences on the other branch. 
(forall (?occ1 ?occ2) (iff (branch_automorphic ?occ1 ?occ2)
(and    (branch_monomorphic ?occ1 ?occ2)
	(branch_monomorphic ?occ2 ?occ1))))
Definition 3 An activity occurrences is permuted iff the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on every other branch. 
(forall (?occ) (iff (permuted ?occ)
(forall (?occ1 ?occ2)
	(if	  (and	(same_grove ?occ1 ?occ)
			(same_grove ?occ2 ?occ))
		  (branch_automorphic ?occ1 ?occ)))))
Definition 4 An activity occurrence is nondeterministically permuted iff the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on some other branch. 
(forall (?occ) (iff (nondet_permuted ?occ)
(forall (?occ1)
	(if	  (same_grove ?occ1 ?occ)
		  (exists (?occ2)
			(and	(same_grove ?occ1 ?occ2)
				(not (= ?occ1 ?occ2))
				(branch_automorphic ?occ1 ?occ2)))))))
Definition 5 An activity occurrence is partially permuted 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 (?occ) (iff (partial_permuted ?occ)
(exists (?occ1 ?occ2 ?occ3)
	(and	(same_grove ?occ1 ?occ)
		(same_grove ?occ2 ?occ)
		(not (= ?occ1 ?occ2))
		(branch_automorphic ?occ1 ?occ2)
		(same_grove ?occ3 ?occ)
		(forall (?occ4)
			(if	  (and	(same_grove ?occ3 ?occ4)
					(branch_automorphic ?occ3 ?occ4))
				  (= ?occ3 ?occ4)))))))
Definition 6 An activity occurrence is simple iff none of the branches in an activity tree are branch automorphic. 
(forall (?occ) (iff (simple ?occ)
(forall (?occ1 ?occ2)
	(if	  (and	(same_grove ?occ1 ?occ)
			(same_grove ?occ2 ?occ)
			(branch_automorphic ?occ1 ?occ2))
		  (= ?occ1 ?occ2)))))