State-based Variation of Complex Activities

State-based Variation of Complex Activities

Extension Name: state_variation.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: variation.def, precondition.def

Grammar: state_variation

Definitions

Definition 1 An activity is conditional iff any two of its minimal activity trees are isomorphic iff the roots agree on state.
(forall (?a) (iff (conditional ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(state_equiv ?occ1 ?occ2))
		(min_equiv ?occ1 ?occ2 ?a)))))
Definition 2 An activity is partial conditional iff there exist isomorphic minimal activity trees that agree on state.
(forall (?a) (iff (partial_conditional ?a)
(and	(exists (?occ1)
		(forall (?occ2)
			(if	  (and	(root ?occ1 ?a)
					(root ?occ2 ?a)
					(state_equiv ?occ1 ?occ2))
				  (min_equiv ?occ1 ?occ2 ?a))))
	(exists (?occ3 ?occ4)
		(and	(root ?occ3 ?a)
			(root ?occ4 ?a)
			(state_equiv ?occ3 ?occ4)
			(not (min_equiv ?occ3 ?occ4 ?a)))))))
Definition 3 An activity is rigid conditional iff for every root occurrence of a minimal activity tree for ?a, there exists another occurrence that agrees on state but which is the root of a nonisomorphic minimal activity tree.
(forall (?a) (iff (rigid_conditional ?a)
(forall (?occ1)
	(exists (?occ2)
		(and	(root ?occ1 ?a)
			(root ?occ2 ?a)
			(state_equiv ?occ1 ?occ2)
			(not (min_equiv ?occ1 ?occ2 ?a)))))))