Extension Name: strong_posets.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: None
Grammar: strongposets.bnf
(forall (?s1 ?s2 ?a) (iff (same_bag ?s1 ?s2 ?a) (exists (?s3 ?s4) (and (next_subocc ?s1 ?s3 ?a) (iso_occ ?s3 ?s2 ?a) (next_subocc ?s2 ?s4 ?a) (iso_occ ?s4 ?s1 ?a)))))Definition 2 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of siblings for ?s.
(forall (?s ?a) (iff (rotate ?s ?a) (and (forall (?s1) (if (next_subocc ?s ?s1 ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a))))) (forall (?s3) (if (sibling ?s ?s3 ?a) (same_bag ?s ?s3 ?a))))))Definition 3 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering.
(forall (?s ?a) (iff (reflect ?s ?a) (forall (?s1) (iff (next_subocc ?s ?s1 ?a) (next_soo (soomap ?s) (soomap ?s1) ?a)))))Definition 4 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering, together with a copy of the siblings of ?s.
(forall (?s ?a) (iff (flip ?s ?a) (forall (?s1) (iff (next_subocc ?s ?s1 ?a) (or (next_soo (soomap ?s) (soomap ?s1) ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a))))))))Definition 5 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering, together with a copy of the siblings of ?s that are in the same bag.
(forall (?s ?a) (iff (turn ?s ?a) (and (exists (?s5) (and (sibling ?s ?s5 ?a) (same_bag ?s ?s5 ?a))) (forall (?s1) (if (next_subocc ?s ?s1 ?a) (or (next_soo (soomap ?s) (soomap ?s1) ?a) (exists (?s2) (and (sibling ?s ?s2 ?a) (iso_occ ?s1 ?s2 ?a)))))))))Definition 6 A bag is an activity tree in which all elements are rotated. Intuitively, this corresponds to a process flow diagram which contains only AND junctions with no linear orderings.
(forall (?occ) (iff (bag ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (rotate ?s ?a)))))Definition 7 A choice poset is an activity tree in which all elements are reflected. Intuitively, this corresponds to a process flow diagram which contains only OR junctions.
(forall (?occ) (iff (choice_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (reflect ?s ?a)))))Definition 8 A strong poset is an activity tree in which all elements are flipped. Intuitively, this corresponds to a process flow diagram which contains linear orderings within AND junctions.
(forall (?occ) (iff (strong_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (flip ?s ?a)))))Definition 9 A complex poset is an activity tree in which all elements are turned. Intuitively, this corresponds to a process flow diagram which contains both AND and OR junctions.
(forall (?occ) (iff (complex_poset ?occ) (forall (?a ?s ?occ1) (if (and (same_grove ?occ ?occ1) (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ1)) (turn ?s ?a)))))