Theory of Resource Requirements

Theory of Resource Requirements

Extension Name: requires.th

Primitive Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: None

Axioms

Axiom 1: 
(forall (?a ?a1 ?r ?s)
	(if  (and	(requires ?a ?r)
			(subactivity ?a1 ?a)
			(atomic ?a1)
			(holds (available ?r ?a1) ?s))
		  (exists (?occ)
			(and	(occurrence_of ?occ ?a)
				(subactivity_occurrence (successor ?a1 ?s) ?occ)))))
Axiom 2: An activity requires a resource if and only if there exists an atomic subactivity that requires the resource. 
(forall (?a ?r)
        (iff    (requires ?a ?r)
                (exists (?a1)
                        (and    (atomic ?a1)
                                (subactivity ?a1 ?a)
                                (requires ?a1 ?r)))))
Axiom 3: A resource is available for an activity iff the available quantity of the resource for the activity exceeds the difference between the quantity of the resource point and the sum of the aggregate demand for the resource and the demand for the resource by the activity. 
(forall (?r ?a ?s)
	(iff	(prior (available ?r ?a) ?s)
		(exists (?q1 ?q2 ?q3)
                        (and	(prior (resource_point ?r ?q1) ?s)
                                (prior (agg_demand ?r ?q3) ?s)
                                (prior (demand ?r ?a ?q2) ?s)
                                (greater ?q1 (plus ?q2 ?q3))))))
Axiom 4: The demand of an activity for a resource must be greater than zero. 
(forall (?r ?a ?q ?s)
	(if  (prior (demand ?r ?a ?q) ?s)
		  (greater ?q zero)))
Axiom 5: The demand of a concurrent superposition of activities for a resource is the sum of the demand of all of its subactivities for the resource. 
(forall (?a1 ?a2 ?r ?q ?s)
	(iff	(prior (demand (conc ?a1 ?a2) ?r ?q) ?s)
		(exists (?q1 ?q2)
                        (and    (prior (demand ?a1 ?r ?q1) ?s)
                                (prior (demand ?a2 ?r ?q2) ?s)
                                (= ?q (plus ?q1 ?q2))))))
Axiom 6: The aggregation of demand for a resource is the sum of demand by all activities which require the resource. Thus, when an activity is initiated, the aggregate demand is incremented by the amount equal to the demand of that acivity for the resource. When the activity is terminated, the aggregate demand is decremented by the amount equal to the demand of the activity for the resource. 
(forall (?r ?q ?s)
	(iff	(holds (agg_demand ?r ?q) ?s)
		(or	(exists (?a1 ?q1 ?q2)
				(and	(occurrence_of ?s ?a1)
					(prior (demand ?r ?a1 ?q1) ?s)
					(prior (agg_demand ?r ?q2) ?s)
					(= ?q (plus ?q1 ?q2))))
			(exists (?a2 ?q1 ?q2)
				(and	(occurrence_of ?s ?a2)
					(prior (demand ?r ?a2 ?q1) ?s)
					(prior (agg_demand ?r ?q2) ?s)
					(= ?q1 (plus ?q ?q2)))))))