Extension Name: repetitive.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: None
Grammar: repetitive.bnf
(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))))))