Resource Sets

Resource Sets

Extension Name: res_set.th

Primitive Lexicon:

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

Definitional Extensions Required by this Extension: None

Axioms

Resource sets are sets whose elements are resources and which are themselves resources for some activity. This is denoted by the fluent function (resource_set ?i ?r), which associates the set ?i with the resource ?r. The actual set associated with the resource may change, as new resources are added or removed. Each resource which is a resource set is associated with a unique set of resources. 
(forall (?i ?r ?occ)
        (if     (holds (resource_set ?i ?r) ?occ)
                (forall (?rp)
                        (if     (set_member ?rp ?i)
                                (exists (?a)
                                        (requires ?a ?rp))))))

(forall (?i ?r1 ?r2 ?a ?occ)
        (if     (and    (holds (resource_set ?i ?r1) ?occ)
                        (set_member ?r2 ?i)
                        (requires ?a ?r2))
                (requires ?a ?r1)))

(forall (?i1 ?i2 ?r ?occ)
        (if     (and    (holds (resource_set ?i1 ?r) ?occ)
                        (holds (resource_set ?i2 ?r) ?occ))
                (= ?i1 ?i2)))

Definitions

A resource ?r1 is in the resource set ?r2 iff ?r1 is an element of the set ?i associated with ?r2. 
(forall (?r1 ?r2 ?occ)
        (iff    (holds (in_resource_set ?r1 ?r2) ?occ)
                (exists (?i)
                        (and    (set_member ?r1 ?i)
                                (holds (resource_set ?i ?r2) ?occ)))))
A resource set ?r1 is a resource subset of a resource set ?r2 iff every element of the set associated with ?r1 is an element of the set associated with ?r2. 
(forall (?r1 ?r2 ?occ)
        (iff    (holds (resource_subset ?r1 ?r2) ?occ)
                (forall (?r ?i1 ?i2)
                   (if  (and    (holds (resource_set ?i1 ?r1) ?occ)
                                (holds (resource_set ?i2 ?r2) ?occ)
                                (set_member ?r ?i1))
                        (set_member ?r ?i2)))))