Variation for Upwards Atomic Activities

Variation for Upwards Atomic Activities

Extension Name: up_variation.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

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

Definitions

Definition 1 An activity is a global filter activity iff every subactivity is has equivalent preconditions whenever the activity is possible. 
(forall (?a) (iff (state_filter ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a1 ?a)
			(poss ?a ?s1)
			(poss ?a ?s2)
			(state_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))
Definition 2 
(forall (?a) (iff (partial_state_filter ?a)
(and    (exists (?s1)
                (forall (?a1 ?s2)
                        (if	  (and	(subactivity ?a1 ?a)
                        		(poss ?a ?s1)
                        		(poss ?a ?s2)
					(state_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a2 ?a)
			(poss ?a ?s3)
			(poss ?a ?s4)
			(state_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))
Definition 3 
(forall (?a) (iff (rigid_state_filter ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (state_equiv ?s1 ?s2)
			(poss ?a ?s1)
			(poss ?a ?s2)
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))
Definition 4 
(forall (?a) (iff (time_filter ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a1 ?a)
			(poss ?a ?s1)
			(poss ?a ?s2)
			(begin_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))
Definition 5 
(forall (?a) (iff (partial_time_filter ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a1 ?a)
                        		(poss ?a ?s1)
                        		(poss ?a ?s2)
					(begin_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a2 ?a)
			(poss ?a ?s3)
			(poss ?a ?s4)
			(begin_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))
Definition 6 
(forall (?a) (iff (rigid_time_filter ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (begin_equiv ?s1 ?s2)
			(poss ?a ?s1)
			(poss ?a ?s2)
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))
Definition 7 An activity is a global filter activity iff every subactivity is has equivalent preconditions whenever the activity is possible. 
(forall (?a) (iff (state_nonfilter ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a1 ?a)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
			(state_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))
Definition 8 
(forall (?a) (iff (partial_state_nonfilter ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a1 ?a)
                        		(not (poss ?a ?s1))
                        		(not (poss ?a ?s2))
					(state_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a2 ?a)
			(not (poss ?a ?s3))
			(not (poss ?a ?s4))
			(state_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))
Definition 9 
(forall (?a) (iff (rigid_state_nonfilter ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (state_equiv ?s1 ?s2)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))
Definition 10 
(forall (?a) (iff (time_nonfilter ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a1 ?a)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
			(begin_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))
Definition 11 
(forall (?a) (iff (partial_time_nonfilter ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a1 ?a)
                        		(not (poss ?a ?s1))
                        		(not (poss ?a ?s2))
					(begin_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a2 ?a)
			(not (poss ?a ?s3))
			(not (poss ?a ?s4))
			(begin_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))
Definition 12 
(forall (?a) (iff (rigid_time_nonfilter ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (begin_equiv ?s1 ?s2)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))