Occurrence-based Effects for Activities

Occurrence-based Effects for Activities

Extension Name: occ_effects.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: effects.def, occ_precond.def

Grammar: occ_effects.bnf

Definitions

Definition 1 An activity has occurrence constrained effects if and only if the effects of the activity are preserved by occurrence tree endomorphisms. 
(forall (?a) (iff (occ_effects ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(tree_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity has occurrence dependent effects if and only if there exist occurrence tree endomorphisms that preserve the effects of the activity. 
(forall (?a) (iff (occ_depend_effects ?a)
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(tree_equiv ?s1 ?s2))
				  (effects_equiv ?a ?s1 ?s2)))))))
Definition 3 An activity has no occurrence dependent effects if and only if the only occurrence tree endomorphism that preserve the effects of the activity is the trivial one. 
(forall (?a) (iff (nonocc_effects ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(tree_equiv ?s1 ?s2)
				(not (effects_equiv ?a ?s1 ?s2))))))))