State-based Distribution of Complex Activities

State-based Distribution of Complex Activities

Extension Name: state_distribution.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: distribution.def, state_precond.def

Grammar: state_distribution.bnf

Definitions

Definition 1 An activity is a trigger activity iff whenever two occurrences agree on state, then they agree on the occurrences of the activity. 
 
(forall (?a) (iff (trigger ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(profile ?occ1 ?a)
			(profile ?occ2 ?a)
			(state_equiv ?occ1 ?occ2))
		  (root_equiv ?a ?occ1 ?occ2)))))
Definition 2 An activity is a partial trigger activity iff there exist occurrences that agree on state and on the occurrence of the activity. 
 
(forall (?a) (iff (partial_trigger ?a)
(and    (exists (?occ1)
                (forall (?occ2)
                        (if	  (and	(profile ?occ1 ?a)
					(profile ?occ2 ?a)
					(state_equiv ?occ1 ?occ2))
                                  (root_equiv ?a ?occ1 ?occ2))))
        (exists (?occ3 ?occ4)
                (and    (profile ?occ3 ?a)
			(profile ?occ4 ?a)
			(state_equiv ?occ3 ?occ4)
                        (not (root_equiv ?a ?occ3 ?occ4)))))))
Definition 3 An activity is a nontrigger activity if and only if the only occurrence-preserving fluent automorphism is the trivial one. 
(forall (?a) (iff (nontrigger ?a)
(forall (?occ1)
	(if	  (profile ?occ1 ?a)
        	  (exists (?occ2)
                	(and    (profile ?occ2 ?a)
				(state_equiv ?occ1 ?occ2)
                        	(not (root_equiv ?a ?occ1 ?occ2))))))))