State-based Effects of Activities

State-based Effects of Activities

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

Grammar: state_effects.bnf

Definitions

Definition 1 An activity is a Markovian effect activity iff whenever any two occurrences of the activity agree on state, then they agree on the effects (i.e. the states that hold after the occurrence. 
 
(forall (?a) (iff (markov_effects ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(state_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a partially state constrained activity if and only if there exist effect-preserving fluent automorphisms. 
(forall (?a) (iff (partial_state_effects ?a)
(and    (exists (?s1)
                (forall (?s2)
                        (if	  (state_equiv ?s1 ?s2)
				  (effects_equiv ?a ?s1 ?s2))))
        (exists (?s3 ?s4)
                (and    (state_equiv ?s3 ?s4)
                        (not (effects_equiv ?a ?s3 ?s4)))))))
Definition 3 An activity is a rigid state activity if and only if the only effects-preserving fluent automorphism is the trivial one. 
(forall (?a) (iff (rigid_state_effects ?a)
(forall (?s1)
        (exists (?s2)
                (and    (state_equiv ?s1 ?s2)
                        (not (effects_equiv ?a ?s1 ?s2)))))))