Homogeneous Sets and Quantity

Homogeneous Sets and Quantity

Extension Name: homogeneous_set.def

Primitive Lexicon: none

Defined Lexicon:

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

Definitional Extensions Required by this Extension: subst_res.def,res_set_action.def, res_divisible.def

Definitions

Definition 1 A homogeneous resource set is a pile with respect to an activity iff it is a homogeneous set with respect to the activity, and the resource point is equal to the cardinality of the set. 
(forall (?a ?r) (iff (pile ?r ?a) 
(and    (homogeneous_set ?r ?a)
        (forall (?q ?occ)
                (iff    (holds (resource_point ?r ?q) ?occ)
                        (exists (?i)
                                (and	(holds (resource_set ?i ?r) ?occ)
                                        (= ?q (cardinality ?i)))))))))
Definition 2 
(forall (?r ?a) (iff (stock ?r ?a) 
(and    (homogeneous_set ?r ?a)
	(forall (?q ?occ)
		(if  (holds (demand ?a ?r ?q) ?occ)
	             (exists (?i1 ?r1)
			(and	(= ?q (cardinality ?i1))
				(holds (resource_set ?i1 ?r1) ?occ)
				(requires_set ?a ?r1)
                                (forall (?q3)
                                    (if  (holds (agg_demand ?r ?q3) ?occ)
                                         (= ?q3 (cardinality ?i1)))))))))))
Definition 3 
(forall (?r ?a) (iff (pool ?r ?a) 
(and    (homogeneous_set ?r ?a)
	(forall (?q ?occ)
		(if  (holds (demand ?a ?r ?q) ?occ)
			  (exists (?i ?i1 ?r1)
				(and	(holds (resource_set ?i ?r) ?occ)
                                        (subset ?i1 ?i)
					(= ?q (cardinality ?i1))
					(holds (resource_set ?i1 ?r1) ?occ)
					(requires_set ?a ?r1))))))))
Definition 4 A pool is used by some activity iff the activity uses some quantity of the resource pool (remember that resource pools are themselves resources). 
(forall (?a ?r ?q) (iff (pool_demand ?a ?r ?q) 
(and	(pool ?r ?a) 
	(forall (?q1 ?occ)
		(if  (holds (demand ?a ?r ?q1) ?occ)
			  (= ?q ?q1))))))
Definition 5 A pile is used by some activity iff the activity uses some quantity of the resource pool (remember that resource pools are themselves resources). 
(forall (?a ?r ?q) (if (uses_pile ?a ?r ?q) 
(and	(pile ?r ?a) 
	(uses_quantity ?a ?r ?q))))
Definition 6 A pile is consumed with respect to some activity iff the activity consumes quantity of resources in the resource pool (remember that resource pools are themselves resources). 
(forall (?a ?r ?q) (iff (consumes_pile ?a ?r ?q) 
(and	(pile ?r ?a) 
	(consumes_quantity ?a ?r ?q))))
Definition 7 A pile is produced with respect to some activity iff the activity produces some quantity of resources in the resource pool (remember that resource pools are themselves resources). 
(forall (?a ?r ?q) (iff (produces_pile ?a ?r ?q) 
(and	(pile ?r ?a) 
	(produces_quantity ?a ?r ?q))))