Folding Branch Structure

Folding Branch Structure

Extension Name: folded.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: folded.bnf

Definitions

Definition 1 One branch of a minimal activity tree is branch-homomorphic to another iff there exists a 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_homomorphic ?occ1 ?occ2)
(and    (same_grove ?occ1 ?occ2)
        (forall (?s1 ?a)
           (if     (and    (occurrence_of ?occ1 ?a)
                           (subactivity_occurrence ?s1 ?occ1))
                   (exists (?s2)
                           (and    (subactivity_occurrence ?s2 ?occ2)
                                   (hom ?s1 ?s2 ?a))))))))
Definition 2 An activity is folded iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?occ) (iff (folded ?occ)
(exists (?occ1)
	(and	(same_grove ?occ1 ?occ)
		(forall (?occ2)
			(if	  (same_grove ?occ2 ?occ)
				  (branch_homomorphic ?occ1 ?occ2)))))))
Definition 3 An activity is nondeterministically folded iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?occ) (iff (nondet_folded ?occ)
(forall (?occ1)
	(if	  (same_grove ?occ1 ?occ)
		  (exists (?occ2)
			(and	(same_grove ?occ2 ?occ)
				(not (= ?occ1 ?occ2))
				(branch_homomorphic ?occ1 ?occ2)))))))
Definition 4 An activity is partially folded iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?occ) (iff (partial_folded ?occ)
(exists (?occ1 ?occ2 ?occ3)
	(and	(same_grove ?occ1 ?occ)
		(same_grove ?occ2 ?occ)
		(not (= ?occ1 ?occ2))
		(branch_homomorphic ?occ1 ?occ2)
		(same_grove ?occ3 ?occ)
		(forall (?occ4)
			(if	  (and	(same_grove ?occ4 ?occ)
					(not (= ?occ3 ?occ4)))
				  (not (branch_homomorphic ?occ3 ?occ4))))))))
Definition 5 An activity is rigid iff none of the branches in an activity tree are branch homomorphic. 
(forall (?occ) (iff (rigid ?occ)
(forall (?occ1 ?occ2)
	(if	  (and	(same_grove ?occ1 ?occ)
			(same_grove ?occ2 ?occ)
			(not (= ?occ1 ?occ2)))
		  (not (branch_homomorphic ?occ1 ?occ2))))))