Repetitive Branch Structure

Repetitive Branch Structure

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

Definitions

Definition 1 The sub-branch of a minimal activity with initial atomic subactivity occurrence ?s1 and final atomic subactivity occurrence ?s2 is occurrence-isomorphic to the sub-branch with initial atomic subactivity occurrence ?s3 and final atomic subactivity occurrence ?s4. 
(forall (?s1 ?s2 ?s3 ?s4 ?a) (iff (branch_mono ?s1 ?s2 ?s3 ?s4 ?a)
(forall (?s5 ?s6)
        (if	  (and  (min_precedes ?s1 ?s5 ?a)
                        (min_precedes ?s6 ?s2 ?a)
                        (next_subocc ?s5 ?s6 ?a))
                  (exists (?s7 ?s8)
                        (and    (min_precedes ?s3 ?s7 ?a)
                                (min_precedes ?s8 ?s4 ?a)
                                (next_subocc ?s7 ?s8 ?a)
                                (iso_occ ?s5 ?s7 ?a)
                                (iso_occ ?s6 ?s8 ?a)))))))
Definition 2 Every atomic subactivity occurrence in ?occ can be embedded in a branch of the subtree whose root occurrence is ?s. 
(forall (?s ?occ) (iff (reptree ?s ?occ)
(forall (?s1 ?a)
	(if	  (and	(occurrence_of ?occ ?a)
			(subactivity_occurrence ?s1 ?occ))
		  (exists (?s2 ?s3 ?s4 ?occ1)
			(and	(same_tree ?occ ?occ1)
				(leaf_occ ?s2 ?occ1)
				(min_precedes ?s3 ?s1 ?a)
				(min_precedes ?s1 ?s4 ?a)
				(branch_mono ?s3 ?s4 ?s ?s2 ?a)))))))
Definition 3 An activity occurrence is repetitive iff every branch in the same activity tree can be embedded in a unique subtree. Intuitively, this is equivalent to the existence of a unique repeating subtree. 
(forall (?occ) (iff (repetitive ?occ)
(exists (?s ?occ2)
	(and	(same_tree ?occ ?occ2)
		(subactivity_occurrence ?s ?occ2)
		(forall (?occ1)
			(if	  (same_tree ?occ ?occ1)
				  (and	(reptree ?s ?occ1)
					(not (= ?s (root_occ ?occ1))))))))))
Definition 4 An activity is nondeterministically repetitive iff every branch in the same activity tree can be embedded in some subtree. Intuitively, this is equivalent to the existence of multiple nonisomorphic repeating subtrees. 
(forall (?occ) (iff (nondet_repetitive ?occ)
(forall (?occ1)
	(if	  (same_tree ?occ ?occ1)
		  (exists (?s ?occ2) 
			(and	(same_tree ?occ ?occ2)
				(subactivity_occurrence ?s ?occ2)
				(reptree ?s ?occ1)
				(not (= ?s (root_occ ?occ1)))))))))
Definition 5 An activity occurrence is partially repetitive iff there exist repeating subtrees, but there also exist branches in the same tree that cannot be mapped to any repeating subtree. 
(forall (?occ) (iff (partial_repetitive ?occ)
(and	(exists (?occ1 ?occ2 ?s)
		(and 	(same_tree ?occ ?occ1)
			(same_tree ?occ ?occ2)
			(subactivity_occurrence ?s ?occ2)
			(rep_tree ?s ?occ1)
			(not (= ?s (root_occ ?occ1)))))
	(exists (?occ1)
		(forall (?s1)
			(if	  (reptree ?s1 ?occ1)
				  (= ?s1 (root_occ ?occ1))))))))
Definition 6 An activity occurrence is amorphous iff there are no repeating subtrees in the same activity tree. 
(forall (?occ) (iff (amorphous ?occ)
(forall (?occ1 ?s)
	(if	  (and	(same_tree ?occ1 ?occ)
			(reptree ?s ?occ1))
		  (= ?s (root_occ ?occ1))))))