Envelopes and Umbrae

Envelopes and Umbrae

Extension Name: envelope.th

Primitive Lexicon:

Relations:

Defined Lexicon: None

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

Definitional Extensions Required by this Extension: embedding.def

Axioms

Axiom 1 Every activity tree has an envelope activity. 
(forall (?a1 ?s)
	(if	  (root ?s ?a1)
		  (exists (?a2)
			(envelope ?a2 ?a1 ?s))))
Axiom 2 Every activity tree has an umbra activity. 
(forall (?a1 ?s)
	(if	  (root ?s ?a1)
		  (exists (?a2)
			(umbra ?a2 ?a1 ?s))))
Axiom 3 Any branch that is a live branch of the envelope is not a dead branch of the original activity. 
(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a2))
		  (not (dead_branch ?s1 ?s ?a1))))
Axiom 4 Any branch that is a live branch of the umbra is not a live branch of the original activity. 
(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a2))
		  (not (live_branch ?s1 ?s ?a1))))
Axiom 5 Any live branch of an activity is a live branch of the envelope. 
(forall (?a1 ?a2 ?s ?s1)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(live_branch ?s1 ?s ?a1))
		  (live_branch ?s1 ?s ?a2)))
Axiom 6 Any dead branch of an activity is a live branch of the umbra. 
(forall (?a1 ?a2  ?s ?s1)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(dead_branch ?s1 ?s ?a1))
		  (live_branch ?s1 ?s ?a2)))
Axiom 7 The envelope for ?a1 is unconstrained on the live branches for ?a1. 
(forall (?a1 ?a2 ?s ?o)
	(if	  (and	(envelope ?a2 ?a1 ?s)
			(occurrence_of ?o ?a2)
			(= ?s (root_occ ?o)))
		  (unrestricted ?o)))
Axiom 8 The umbra for ?a1 is unconstrained on the dead branches for ?a1. 
 
(forall (?a1 ?a2 ?s ?o)
	(if	  (and	(umbra ?a2 ?a1 ?s)
			(occurrence_of ?o ?a2)
			(= ?s (root_occ ?o)))
		  (unrestricted ?o)))