Reasoning about Resource Divisibility

Reasoning about Resource Divisibility

Extension Name: res_divisible.def

Primitive Lexicon: None

Defined Lexicon:

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

Definitional Extensions Required by this Extension: none

Definitions

It is important to realize that the notion of quantity referred to in this extension is independent of the notion of resource existence or identity, as well as the distinction between discrete and continuous resources. We are only concerned with the availability of the resource for a future activity. The notion of resource point is a constraint on such availability. The quantity specifies the divisibility of the resource with respect to multiple concurrent activities. The resource point determines the maximal set of concurrent activities which require the resource. Thus, if the quantity is zero, then no activity that requires the resource is possible. Definition 1 An activity consumes some quantity ?q of a resource iff the demand for the resource is ?q and the resource point of the resource is decremented by ?q after the occurrence of the activity. 
(forall (?a ?r ?q) (iff (consumes_quantity ?a ?r ?q) 
(forall (?q1 ?occ1 ?occ2)
	(if  (and	(do ?a ?occ1 ?occ2)
			(holds (demand ?a ?r ?q) ?occ1)
			(holds (resource_point ?r ?q1) ?occ1))
		  (holds (resource_point ?r (minus ?q1 ?q)) ?occ2)))))
Definition 2 An activity strictly consumes some quantity of a resource if the resource is nonreplenishable. 
(forall (?a ?r ?q) (iff (strict_consumes_quantity ?a ?r ?q) 
(and	(consumes_quantity ?a ?r ?q)
	(nonreplenishable ?r))))
Definition 3 An activity produces some quantity ?q of a resource iff the resource point of the resource is incremented by ?q after the occurrence of the activity. 
(forall (?a ?r ?q) (iff (produces_quantity ?a ?r ?q) 
(forall (?q1 ?q2 ?occ1 ?occ2)
	(if  (and	(do ?a ?occ1 ?occ2)
			(holds (resource_point ?r ?q1) ?occ1)
			(= ?q2 (plus ?q1 ?q)))
	  	  (holds (resource_point ?r ?q2) ?occ2)))))
Definition 4 An activity strictly produces some quantity of a resource if there is no other activity that consumes some quantity of it. 
(forall (?a ?r ?q) (iff (strict_produces_quantity ?a ?r ?q) 
(and	(produces_quantity ?a ?r ?q)
	(not (exists (?a2 ?q2)
		(and	(subactivity ?a2 ?a)
			(consumes_quantity ?a2 ?r ?q2)))))))
Definition 5 An activity uses some quantity ?q of a resource iff the demand for the resource is ?q and the resource point of the resource is unchanged by the occurrence of the activity. 
(forall (?a ?r ?q) (iff (uses_quantity ?a ?r ?q) 
(forall (?q1 ?q2 ?occ1 ?occ2)
	(if  (and	(do ?a ?occ1 ?occ2)
			(holds (demand ?a ?r ?q) ?occ1)
			(holds (resource_point ?r ?q1) ?occ1)
			(holds (resource_point ?r ?q2) ?occ2))
		  (= ?q2 ?q1)))))
Definition 6 An activity creates a resource if it produces some quantity of the resource, and the quantity of the resource before the occurrence of the activity was zero. 
(forall (?a ?r) (iff (creates ?a ?r) 
(exists (?q1)
	(and    (produces_quantity ?a ?r ?q1)
        	(forall (?q2 ?occ)
                	(if  (and	(occurrence_of ?occ ?a)
                                	(prior (resource_point ?r ?q2) ?occ))
                             (= ?q2 0)))))))
Definition 7 An activity destroys a resource if it consumes some quantity of the resource, and the quantity of the resource after the occurrence of the activity is zero. 
(forall (?a ?r) (iff (destroys ?a ?r) 
(exists (?q1)
	(and    (consumes_quantity ?a ?r ?q1)
        	(forall (?q2 ?occ)
                	(if  (and	(occurrence_of ?occ ?a)
                                	(prior (resource_point ?r ?q2) ?occp))
                             (= ?q2 0)))))))
Definition 7 A resource has fixed quantity ?q iff the resource point of the resource is the same in all situations i.e. it does not change. 
(forall (?r ?q) (iff (fixed_quantity ?r ?q) 
(forall (?occ)
	(holds (resource_point ?r ?q) ?occ))))
Definition 8 A resource is nonreplenishable iff the resource point for the resource cannot be increased after the occurrence of activities that require the resource. 
(forall (?r) (iff (nonreplenishable ?r) 
(forall (?a ?q1 ?q2 ?occ1 ?occ2 ?occ3)
	(if  (and	(if  (do ?a ?occ1 ?occ2)
				  (holds (resource_point ?r ?q1) ?occ2))
			(precedes ?occ2 ?occ3)
			(holds (resource_point ?r ?q2) ?occ3))
		  (lesserEq q2 ?q1)))))
Definition 9 An activity uses a resource if it uses some quantity of the resource. 
(forall (?a ?r) (iff (uses ?a ?r) 
(exists (?q)
	(uses_quantity ?a ?r ?q))))
Definition 10 An activity consumes a resource if it consumes some quantity of the resource. 
(forall (?a ?r) (iff (consumes ?a ?r) 
(exists (?q)
	(consumes_quantity ?a ?r ?q))))
Definition 11 An activity strictly consumes a resource if it strictly consumes some quantity of the resource. 
(forall (?a ?r) (iff (strict_consumes ?a ?r) 
(exists (?q)
	(strict_consumes_quantity ?a ?r ?q))))
Definition 12 An activity produces a resource if it produces some quantity of the resource. 
(forall (?a ?r) (iff (produces ?a ?r) 
(exists (?q)
	(produces_quantity ?a ?r ?q))))
Definition 13 An activity strictly produces a resource if it strictly produces some quantity of the resource. 
(forall (?a ?r) (iff (strict_produces ?a ?r) 
(exists (?q)
	(strict_produces_quantity ?a ?r ?q))))
Definition 14 An activity provides some quantity of a resource if there exists a subactivity that produces some quantity of the resource and another subactivity that consumes some quantity of the resource. 
(forall (?a ?r ?q) (iff (provides_quantity ?a ?r ?q) 
(and	(exists (?a1)
		(and	(subactivity ?a1 ?a)
			(produces_quantity ?a1 ?r ?q)))
	(exists (?a2)
		(and	(subactivity ?a2 ?a)
			(consumes_quantity ?a2 ?r ?q))))))
Definition 15 An activity provides a resource if it provides some quantity of a resource. 
(forall (?a ?r) (iff (provides ?a ?r) 
(exists (?q)
	(provides_quantity ?a ?r ?q))))