Occurrence-based Preconditions for Activities

Occurrence-based Preconditions for Activities

Extension Name: occ_precond.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: occtree.th, psl_core.th

Definitional Extensions Required by this Extension: precond.def

Grammar: occ_precond.bnf

Definitions

Definition 1 Two activity occurrences are tree equivalent if only if they are in the same orbit of the group space in which the tree-preserving group acts on the legal occurrence tree. 
(forall (?a ?s1 ?s2)
(iff	(tree_equiv (successor ?a ?s1) (successor ?a ?s2))
	(and	(legal_equiv ?s1 ?s2)
		(or	(tree_equiv ?s1 ?s2)
			(initial ?s1)
			(initial ?s2)))))
Definition 2 An activity is occurrence constrained if and only if all occurrence tree endomorphisms preserve legal occurrences of the activity. 
(forall (?a) (iff (occurrence_constrained ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(tree_equiv ?s1 ?s2))
		  (legal_equiv ?s1 ?s2)))))
Definition 3 An activity is occurrence dependent if and only if there exist occurrence tree endomorphisms that preserve legal occurrences of the activity. 
(forall (?a) (iff (occurrence_dependent ?a)
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(tree_equiv ?s1 ?s2))
				  (legal_equiv ?s1 ?s2)))))))
Definition 4 An activity is occurrence independent if and only if there is no nontrivial occurrence tree endomorphism that preserves legal occurrences of the activity. 
(forall (?a) (iff (occurrence_independent ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(tree_equiv ?s1 ?s2)
				(not (legal_equiv ?s1 ?s2))))))))