Preventable Preconditions for Activities

Preventable Preconditions for Activities

Extension Name: preventable.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: occ_precond.def, state_precond.def, precond.def

Grammar: preventable.bnf

Definitions

Definition 1 An activity is preventable if and only if legal occurrences depend on the fluents that hold at other activity occurrences in the tree. In particular, activity occurrences that are in the same orbit of occurrence tree endormorphisms are also in the same orbit of fluent automorphisms. 
(forall (?a) (iff (preventable ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(state_equiv ?s1 ?s2)
			(tree_equiv ?s1 ?s2))
		  (legal_equiv ?s1 ?s2)))))
Definition 2 An activity is possibly preventable if and only if legal occurrences depend on the fluents that hold at other activity occurrences in the tree. In particular, there exist activity occurrences that are in the same orbit of occurrence tree endormorphisms that are also in the same orbit of fluent automorphisms. 
(forall (?a) (iff (possibly_preventable ?a) 
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(state_equiv ?s1 ?s2)
					(tree_equiv ?s1 ?s2))
				  (legal_equiv ?s1 ?s2)))))))
Definition 3 An activity is unpreventable if and only if there is no relationship between legal occurrences and the fluents that hold at other activity occurrences. In particular, the only occurrence tree endomorphism that preserves fluents is the trivial one. 
(forall (?a) (iff (unpreventable ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(state_equiv ?s1 ?s2)
				(tree_equiv ?s1 ?s2)
				(not (legal_equiv ?s1 ?s2))))))))