Spectrum for Atomic Activities

Extension Name: atomic_spectra.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

(global_ideal ?a)
(global_nonideal ?a)
(global_filter ?a)
(global_nonfilter ?a)

Definitional Extensions Required by this Extension: precond.def

Definitions

Definition 1

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

Definition 2

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

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

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

Definition 4

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