Subactivity Occurrence Ordering

Subactivity Occurrence Ordering

Extension Name: soo.th

Primitive Lexicon:

Relations:

Functions: 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

Axioms

Axiom 1 The soo_precedes relation orders elements of the subactivity occurrence ordering. 
(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)))

Definitions

Definition 1 An activity occurrence is a root 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 precedes it in the ordering. 
(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)))))))