Classes of Atomic Activities

Extension Name: concurrent.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

(superpose ?a ?s)
(assistance ?a ?s)
(team ?a ?s)
(ghost ?a ?s)
(conflict ?a ?s)
(dysfunction ?a ?s)

Definitional Extensions Required by this Extension: None

Definitions

An activity is a superposition activity iff every subactivity is possible whenever the activity itself is possible.

(forall (?a ?s) (iff (superpose ?a ?s)
(forall (?a1)
	(if	  (and	(subactivity ?a1 ?a)
			(poss ?a ?s))
		  (poss ?a1 ?s)))))

An activity is an assistance activity iff

(forall (?a ?s) (iff (assistance ?a ?s)
(forall (?a1 ?a2)
	(if	  (and	(subactivity ?a1 ?a)
			(subactivity ?a2 ?a)
			(poss ?a ?s))
		  (poss (conc ?a1 ?a2) ?s)))))

(forall (?a ?s) (iff (team ?a ?s)
(exists (?a1 ?a2)
	(and	(subactivity ?a1 ?a)
		(subactivity ?a2 ?a)
		(poss ?a ?s)
		(not (poss (conc ?a1 ?a2) ?s))))))

(forall (?a ?s) (iff (ghost ?a ?s)
(forall (?a1)
	(if	  (and	(subactivity ?a1 ?a)
			(poss ?a1 ?s))
		  (poss ?a ?s)))))

(forall (?a ?s) (iff (conflict ?a ?s)
(forall (?a1 ?a2)
	(if	  (and	(subactivity ?a1 ?a)
			(subactivity ?a2 ?a)
			(not (poss ?a1 ?s))
			(poss (conc ?a1 ?a2) ?s))
		  (poss ?a ?s)))))

(forall (?a ?s) (iff (dysfunction ?a ?s)
(exists (?a1 ?a2)
	(and	(subactivity ?a1 ?a)
		(subactivity ?a2 ?a)
		(not (poss ?a1 ?s))
		(not (poss ?a ?s))
		(poss (conc ?a1 ?a2) ?s)))))