Variation for Downwards 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:

(state_ideal ?a)
(partial_state_ideal ?a)
(rigid_state_ideal ?a)
(time_ideal ?a)
(partial_time_ideal ?a)
(rigid_time_ideal ?a)
(state_nonideal ?a)
(partial_state_nonideal ?a)
(rigid_state_nonideal ?a)
(time_nonideal ?a)
(partial_time_nonideal ?a)
(rigid_time_nonideal ?a)

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

Definitions

Definition 1 An activity is a global ideal activity iff every subactivity is has equivalent preconditions whenever the activity is possible.

(forall (?a) (iff (state_ideal ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a ?a1)
			(poss ?a ?s1)
			(poss ?a ?s2)
			(state_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))

Definition 2

(forall (?a) (iff (partial_state_ideal ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a ?a1)
                        		(poss ?a ?s1)
                        		(poss ?a ?s2)
					(state_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a ?a2)
			(poss ?a ?s3)
			(poss ?a ?s4)
			(state_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))

Definition 3

(forall (?a) (iff (rigid_state_ideal ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (state_equiv ?s1 ?s2)
			(subactivity ?a ?a1)
			(poss ?a ?s1)
			(poss ?a ?s2)
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))

Definition 4

(forall (?a) (iff (time_ideal ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a ?a1)
			(poss ?a ?s1)
			(poss ?a ?s2)
			(begin_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))

Definition 5

(forall (?a) (iff (partial_time_ideal ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a ?a1)
                        		(poss ?a ?s1)
                        		(poss ?a ?s2)
					(begin_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a ?a2)
			(poss ?a ?s3)
			(poss ?a ?s4)
			(begin_equiv ?s3 ?s4)
                        (not (poss_equiv ?a2 ?s3 ?s4)))))))

Definition 6

(forall (?a) (iff (rigid_time_ideal ?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 ideal activity iff every subactivity is has equivalent preconditions whenever the activity is possible.

(forall (?a) (iff (state_nonideal ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a ?a1)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
			(state_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))

Definition 8

(forall (?a) (iff (partial_state_nonideal ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a ?a1)
                        		(not (poss ?a ?s1))
                        		(not (poss ?a ?s2))
					(state_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a ?a2)
			(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_nonideal ?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_nonideal ?a)
(forall (?a1 ?s1 ?s2)
	(if	  (and	(subactivity ?a ?a1)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
			(begin_equiv ?s1 ?s2))
		  (poss_equiv ?a1 ?s1 ?s2)))))

Definition 11

(forall (?a) (iff (partial_time_nonideal ?a)
(and    (exists (?s1)
                (forall (?s2 ?a1)
                        (if	  (and	(subactivity ?a ?a1)
                        		(not (poss ?a ?s1))
                        		(not (poss ?a ?s2))
					(begin_equiv ?s1 ?s2))
                                  (poss_equiv ?a1 ?s1 ?s2))))
        (exists (?a2 ?s3 ?s4)
                (and    (subactivity ?a ?a2)
			(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_nonideal ?a)
(forall (?s1)
        (exists (?a1 ?s2)
                (and    (begin_equiv ?s1 ?s2)
			(subactivity ?a ?a1)
			(not (poss ?a ?s1))
			(not (poss ?a ?s2))
                        (not (poss_equiv ?a1 ?s1 ?s2)))))))