Extension Name: soo.th
Primitive Lexicon:
Relations:
Relations:
Definitional Extensions Required by this Extension: none
(forall (?s1 ?s2 ?a) (if (soo_precedes ?s1 ?s2 ?a) (and (soo ?s1 ?a) (soo ?s2 ?a))))Axiom 2 Elements of the subactivity occurrence ordering are elements of the activity tree.
(forall (?a ?s) (if (soo ?s ?a) (or (root ?s ?a) (exists (?s1) (min_precedes ?s1 ?s ?a)))))Axiom 3 The function soomap maps the activity tree to the subactivity occurrence ordering.
(forall (?s ?occ ?a) (if (and (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ) (arboreal ?s)) (soo (soomap ?s) ?a)))Axiom 4 The elements of the subactivity occurrence ordering are fixed by soomap.
(forall (?s ?a) (if (soo ?s ?a) (= ?s (soomap ?s))))Axiom 5 The function soomap is a branch monomorphism.
(forall (?s ?a) (or (mono ?s (soomap ?s) ?a) (= ?s (soomap ?s))))Axiom 6 The activity tree is order-homomorphic to the subactivity occurrence ordering.
(forall (?a ?s1 ?s2) (if (min_precedes ?s1 ?s2 ?a) (iff (soo_precedes (soomap ?s1) (soomap ?s2) ?a) (not (exists (?s3 ?s4) (and (min_precedes ?s4 ?s3 ?a) (= (soomap ?s3) (soomap ?s1)) (= (soomap ?s4) (soomap ?s2))))))))Axiom 7 soo_precedes is not symmetric.
(forall (?a ?s1 ?s2) (if (soo_precedes ?s1 ?s2 ?a) (not (soo_precedes ?s2 ?s1 ?a))))Axiom 8 soo_precedes is transitive.
(forall (?a ?s1 ?s2 ?s3) (if (and (soo_precedes ?s1 ?s2 ?a) (soo_precedes ?s2 ?s3 ?a)) (soo_precedes ?s1 ?s3 ?a)))
(forall (?s ?a) (iff (root_soo ?s ?a) (and (soo ?s ?a) (not (exists (?s1) (soo_precedes ?s1 ?s ?a))))))Definition 2 An activity occurrence is a leaf of a subactivity occurrence ordering for an activity ?a if and only if it is an element of the ordering and there does not exist an activity occurrence that follows it in the ordering.
(forall (?s ?a) (iff (leaf_soo ?s ?a) (and (soo ?s ?a) (not (exists (?s1) (soo_precedes ?s ?s1 ?a))))))Definition 3 An activity occurrence ?s2 is the next subactivity occurrence after ?s1 in a subactivity occurrence ordering for ?a if and only of ?s1 precedes ?s2 in the ordering and there does not exist a subactivity occurrence that is between them in the ordering.
(forall (?s1 ?s2 ?a) (iff (next_subactivity ?s1 ?s2 ?a) (and (soo_precedes ?s1 ?s2 ?a) (not (exists (?s3) (and (soo_precedes ?s1 ?s3 ?a) (soo_precedes ?s3 ?s2 ?a)))))))