Duration-based Effects of Activities

Duration-based Effects of Activities

Extension Name: dur_effects.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

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

Grammar: dur_effects.bnf

Definitions

Definition 1 An activity is a duration effect activity iff whenever any two occurrences of the activity agree on their duration, then they agree on the effects (i.e. the states that hold after the occurrence). 
 
(forall (?a) (iff (duration_effects ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(dur_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a partially duration constrained activity if and only if there exist effect-preserving duration automorphisms. 
(forall (?a) (iff (partial_duration_effects ?a) 
(and    (exists (?s1)
                (forall (?s2)
                        (if	  (and	(occurrence_of ?s1 ?a)
					(occurrence_of ?s2 ?a)
					(dur_equiv ?s1 ?s2))
				  (effects_equiv ?a ?s1 ?s2))))
        (exists (?s3 ?s4)
                (and    (occurrence_of ?s3 ?a)
			(occurrence_of ?s4 ?a)
			(dur_equiv ?s3 ?s4)
                        (not (effects_equiv ?a ?s3 ?s4)))))))
Definition 3 An activity is a nonduration effects activity if and only if the only effects-preserving duration automorphism is the trivial one. 
(forall (?a) (iff (nonduration_effects ?a) 
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
        	  (exists (?s2)
                	(and    (occurrence_of ?s2 ?a)
				(dur_equiv ?s1 ?s2)
                        	(not (effects_equiv ?a ?s1 ?s2))))))))