Spoilage Activities

Spoilage Activities

Extension Name: spoilage.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

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

Grammar: spoilage.bnf

Definitions

Definition 1 An activity is a spoilage if and only if legal occurrences depend on the delay between other activity occurrences. In particular, activity occurrences that are in the same orbit of occurrence tree endormorphisms are also in the same orbit of delay automorphisms. 
(forall (?a) (iff (spoilage ?a) 
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(delay_equiv ?s1 ?s2)
			(tree_equiv ?s1 ?s2))
		  (legal_equiv ?s1 ?s2)))))
Definition 2 An activity is possible spoilage if and only if there exist activity occurrences that are in the same orbit of occurrence tree endormorphisms and that are also in the same orbit of delay automorphisms. 
(forall (?a) (iff (possible_spoilage ?a) 
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(delay_equiv ?s1 ?s2)
					(tree_equiv ?s1 ?s2))
				  (legal_equiv ?s1 ?s2)))))))
Definition 3 An activity is nonspoilage if and only if there is no relationship between legal occurrences and the delay between other activity occurrences. In particular, the only occurrence tree endomorphism that preserves the delay between other activity occurrences is the trivial one. 
(forall (?a) (iff (nonspoilage ?a) 
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(delay_equiv ?s1 ?s2)
				(tree_equiv ?s1 ?s2)
				(not (legal_equiv ?s1 ?s2))))))))