Interruptable Activities

Extension Name: interrupt.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

(cathode ?a ?s)
(anode ?a ?s)
(interruptable ?a ?s)
(uninterruptable ?a ?s)
(separatable ?a ?s)

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

Definitional Extensions Required by this Extension: None

Definitions

Definition 1

(forall (?a ?s) (iff (cathode ?a ?s) 
(forall (?a1 ?a2 ?occ1 ?occ2 ?s1 ?s2)
	(if	  (and	(envelope ?a1 ?a ?s)
			(umbra ?a2 ?a ?s)
			(occurrence_of ?occ1 ?a1)
			(occurrence_of ?occ2 ?a2)
			(= ?s (root_occ ?occ1))
			(= ?s (root_occ ?occ2))
			(next_subocc ?s1 ?s2 ?occ1))
		  (exists (?S3 ?s4)
			(and	(iso_occ ?s1 ?s3)
				(iso_occ ?s2 ?s4)
				(next_subocc ?s3 ?s4 ?occ2)))))))

Definition 2

(forall (?a ?s) (iff (anode ?a ?s) 
(forall (?a1 ?a2 ?occ1 ?occ2 ?s1 ?s2)
	(if	  (and	(envelope ?a1 ?a ?s)
			(umbra ?a2 ?a ?s)
			(occurrence_of ?occ1 ?a1)
			(occurrence_of ?occ2 ?a2)
			(= ?s (root_occ ?occ1))
			(= ?s (root_occ ?occ2))
			(next_subocc ?s1 ?s2 ?occ2))
		  (exists (?S3 ?s4)
			(and	(iso_occ ?s1 ?s3)
				(iso_occ ?s2 ?s4)
				(next_subocc ?s3 ?s4 ?occ1)))))))

Definition 3

(forall (?a ?s) (iff (interruptable ?a ?s) 
(and	(anode ?a ?s)
	(not (cathode ?a ?s)))))

Definition 4

(forall (?a ?s) (iff (interruptable ?a ?s) 
(and	(not (anode ?a ?s))
	(cathode ?a ?s))))

Definition 5

(forall (?a ?s) (iff (separatable ?a ?s) 
(and	(not (anode ?a ?s))
	(not (cathode ?a ?s)))))