Effects of Activities based on Duration and State

Effects of Activities based on Duration and State

Extension Name: maintain_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.th, effects.def, state_precond.def

Grammar: maintain_effects.bnf

Definitions

Definition 1 An activity is a maintain effect activity iff whenever any two occurrences of the activity agree on their duration and their state, then they agree on the effects (i.e. the states that hold after the occurrence). 
 
(forall (?a) (iff (maintain_effects ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(state_equiv ?s1 ?s2)
			(dur_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a partially maintained activity if and only if there exist effect-preserving automorphisms that preserve both duration and state. 
(forall (?a) (iff (partial_maintain ?a) 
(and    (exists (?s1)
                (forall (?s2)
                        (if	  (and	(occurrence_of ?s1 ?a)
					(occurrence_of ?s2 ?a)
					(state_equiv ?s1 ?s2)
					(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 nonmaintain effects activity if and only if the only effects-preserving duration and fluent automorphism is the trivial one. 
(forall (?a) (iff (nonmaintain ?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))))))))