Skeletal Activity Trees

Skeletal Activity Trees

Extension Name: skeletal.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

Definitional Extensions Required by this Extension: embedding.def

Grammar: skeletal.bnf

Definitions

Definition 1 An activity occurrence ?occ is fused if and only if every activity occurrence between a root and a leaf occurrence is also a subactivity occurrence of ?occ. 
(forall (?occ) (iff (fused ?occ) 
(forall (?s1 ?s2 ?s3)
	(if	  (and	(= ?s1 (root_occ ?occ))
			(subactivity_occurrence ?s2 ?occ)
			(precedes ?s1 ?s3)
			(precedes ?s3 ?s2))
		  (subactivity_occurrence ?s3 ?occ)))))
Definition 2 The branch of the occurrence tree containing the activity occurrence ?occ can be embedded into a dead branch in the same maximal embedded subtree. 
(forall (?occ) (iff (embed_occ ?occ)
(forall (?a ?s ?s1 ?s2 ?s3)
	(if	  (and	(occurrence_of ?occ ?a)
			(= ?s (root_occ ?occ))
			(next_subocc ?s1 ?s2 ?occ)
			(precedes ?s1 ?s3)
			(precedes ?s3 ?s2))
		  (exists (?s4 ?s5 ?s6)
			(and	(precedes ?s4 ?s5)
				(precedes ?s5 ?s6)
				(iso_occ ?s4 ?s1 ?a)
				(iso_occ ?s5 ?s3 ?a)
				(iso_occ ?s6 ?s3 ?a)
				(dead_branch ?s1 ?s4 ?a)
				(dead_branch ?s1 ?s6 ?a)))))))
Definition 3 An activity occurrence is free if and only if there exist activity occurrences in the same tree that are fused and there exist activity occurrences that are not fused. This is equivalent to saying that there do not exist necessary external activity occurrences. 
(forall (?occ) (iff (free ?occ)
(exists (?occ1 ?occ2)
	(and	(same_tree ?occ ?occ1)
		(same_tree ?occ ?occ2)
		(not (fused ?occ1))
		(fused ?occ2)))))
Definition 4 An activity occurrence is assisted if and only if every activity occurrence in the same tree are not fused. This is equivalent to saying that there exist necessary external activity occurrences. 
(forall (?occ) (iff (assisted ?occ)
(forall (?occ1)
	(if	  (same_tree ?occ ?occ1)
		  (not (fused ?occ1))))))
Definition 5 An activity is helpless if and only if between any two subactivity occurrences, there exists an external activity occurrence. This is equivalent to saying that external activities are always necessary. 
(forall (?occ) (iff (helpless ?occ)
(forall (?s1 ?s2)
	(if	  (next_subocc ?s1 ?s2 ?occ)
		  (exists (?s3)
			(and	(precedes ?s1 ?s3)
				(precedes ?s3 ?s2)
				(not (subactivity_occurrence ?s3 ?occ))))))))
Definition 6 An activity occurrence is unbound if and only if none of the activity occurrences in the same tree can be embedded into dead branches. This is equivalent to the nonexistence of forbidden external activities. 
(forall (?occ) (iff (unbound ?occ)
(forall (?occ1)
	(if	  (same_tree ?occ1 ?occ)
		  (not (embed_occ ?occ1))))))
Definition 7 An activity occurrence is bound if and only if there exist activity occurrences in the same tree that can be embedded into dead branches. This is equivalent to the existence of forbidden external activities. 
(forall (?occ) (iff (bound ?occ)
(exists (?occ1 ?occ2)
	(and	(same_tree ?occ1 ?occ)
		(not (embed_occ ?occ1))
		(same_tree ?occ2 ?occ)
		(embed_occ ?occ2)))))
Definition 8 An activity occurrence is strict if and only if all accurrences in the same tree are fused. This is equivalent to saying that all external activity occurrences are forbidden. 
(forall (?occ) (iff (strict ?occ)
(forall (?occ1)
	(if	  (same_tree ?occ ?occ1)
		  (fused ?occ1)))))