Effects of Activities: Occurrence Constraints

Effects of Activities: Occurrence Constraints

Extension Name: quantum.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

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

Grammar: quantum.bnf

Definitions

Definition 1 An activity is a quantum activity if and only if its effects depend on the fluents that hold at other activity occurrences in the tree. In particular, effects are preserved by occurrence tree endomorphisms that also preserve fluents. 
(forall (?a) (iff (quantum ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(state_equiv ?s1 ?s2)
			(tree_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a semiclassical activity if and only if there exist occurrence tree endomorphisms that also preserve fluents and the effects of the activity. 
(forall (?a) (iff (semiclassical ?a)
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(state_equiv ?s1 ?s2)
					(tree_equiv ?s1 ?s2))
				  (effects_equiv ?a ?s1 ?s2)))))))
Definition 3 An activity is classical if and only if its effects are independent of the occurrences of any other activities in the occurrence tree. 
(forall (?a) (iff (classical ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(state_equiv ?s1 ?s2)
				(tree_equiv ?s1 ?s2)
				(not (effects_equiv ?a ?s1 ?s2))))))))