Effects of Activities: Temporal and Occurrence Constraints

Effects of Activities: Temporal and Occurrence Constraints

Extension Name: relativistic.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: occ_precond.def, effects.def, time_precond.def

Grammar: relativistic.bnf

Definitions

Definition 1 An activity is relativistic if and only if its effects depend on the timepoints at which other activities occur in the tree. In particular, effects are preserved by occurrence tree endomorphisms that also preserve the timeline. 
(forall (?a) (iff (relativistic ?a)
(forall (?s1 ?s2)
	(if	  (and	(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a)
			(begin_equiv ?s1 ?s2)
			(tree_equiv ?s1 ?s2))
		  (effects_equiv ?a ?s1 ?s2)))))
Definition 2 An activity is a seminewton activity if and only if there exist occurrence tree endomorphisms that also preserve the timeline and the effects of the activity. 
(forall (?a) (iff (seminewton ?a)
(exists (?s1)
	(and	(occurrence_of ?s1 ?a)
		(forall (?s2)
			(if	  (and	(occurrence_of ?s2 ?a)
					(begin_equiv ?s1 ?s2)
					(tree_equiv ?s1 ?s2))
				  (effects_equiv ?a ?s1 ?s2)))))))
Definition 3 An activity is newtonian if and only if its effects are independent of the beginof timepoints of occurrences of any other activities in the occurrence tree. 
(forall (?a) (iff (newtonian ?a)
(forall (?s1)
	(if	  (occurrence_of ?s1 ?a)
		  (exists (?s2)
			(and	(occurrence_of ?s2 ?a)
				(begin_equiv ?s1 ?s2)
				(tree_equiv ?s1 ?s2)
				(not (effects_equiv ?a ?s1 ?s2))))))))