Complex Activity Occurrence Orderings

Complex Activity Occurrence Orderings

Extension Name: coo.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: soo.th, act_occ.th, complex.th, atomic.th, subactivity.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: strongposets.def

Grammar: coo.bnf

Definitions

Definition 1 A complex activity occurrence ?occ1 coo_precedes a complex activity occurrence ?occ2 iff every atomic subactivity occurrence of ?occ1 soo_precedes every atomic subactivity occurrence of ?occ2. 
(forall (?occ1 ?occ2 ?a) (iff (coo_precedes ?occ1 ?occ2 ?a)
(forall (?s1 ?s2)
	(if	  (and	(subactivity_occurrence ?s1 ?occ1)
			(subactivity_occurrence ?s2 ?occ2)
			(atomocc ?s1)
			(atomocc ?s2))
		  (soo_precedes ?s1 ?s2 ?a)))))
Definition 2 A complex activity occurrence ?occ1 is strong_parallel with a complex activity occurrence ?occ2 iff any atomic subactivity occurrence of ?occ1 is in the same bag as an atomic subactivity occurrence of ?occ2. 
(forall (?occ1 ?occ2 ?a) (iff (strong_parallel ?occ1 ?occ2 ?a)
(forall (?s1 ?s2)
	(if	  (and	(subactivity_occurrence ?s1 ?occ1)
			(subactivity_occurrence ?s2 ?occ2)
			(atomocc ?s1)
			(atomocc ?s2))
		  (same_bag ?s1 ?s2 ?a)))))
Definition 3 An activity occurrence is atomocc iff it is the occurrence of an atomic activity. 
(forall (?s) (iff (atomocc ?s)
(exists (?a)
	(and	(atomic ?a)
		(occurrence_of ?s ?a)))))