;; Extension Name: psl_core.th
;; Primitive Lexicon:
;; Relations: ;;
;; Relations: ;;
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?t1 ?t2) (=> (before ?t1 ?t2) (and (timepoint ?t1) (timepoint ?t2)))) ;;;; Axiom 2 The before relation is a total ordering. ;;
(forall (?t1 ?t2) (=> (and (timepoint ?t1) (timepoint ?t2)) (or (equal ?t1 ?t2) (before ?t1 ?t2) (before ?t2 ?t1)))) ;;;; Axiom 3 The before relation is irreflexive. ;;
(forall (?t1) (not (before ?t1 ?t1))) ;;;; Axiom 4 The before relation is transitive. ;;
(forall (?t1 ?t2 ?t3) (=> (and (before ?t1 ?t2) (before ?t2 ?t3)) (before ?t1 ?t3))) ;;;; Axiom 5 The timepoint inf- is before all other timepoints. ;;
(forall (?t)
(=> (and (timepoint ?t)
(not (equal ?t inf-)))
(before inf- ?t)))
;;
;; Axiom 6 Every other timepoint is before inf+.
;;
(forall (?t)
(=> (and (timepoint ?t)
(not (equal ?t inf+)))
(before ?t inf+)))
;;
;; Axiom 7 Given any timepoint t other than inf-, there is a timepoint between
;; inf- and t.
;; (forall (?t) (=> (and (timepoint ?t) (not (equal ?t inf-))) (exists (?u) (between inf- ?u ?t)))) ;;;; Axiom 8 Given any timepoint t other than inf+, there is a timepoint between ;; t and inf+. ;;
(forall (?t) (=> (and (timepoint ?t) (not (equal ?t inf+))) (exists (?u) (between ?t ?u inf+)))) ;;;; Axiom 9 Everything is either an activity, activity occurrence, timepoint, ;; or object. ;;
(forall (?x) (or (activity ?x) (activity_occurrence ?x) (timepoint ?x) (object ?x))) ;;;; Axiom 10 Objects, activities, activity occurrences, and timepoints are all ;; distinct kinds of things. ;;
(forall (?x)
(and (=> (activity ?x)
(not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))
(=> (activity_occurrence ?x)
(not (or (object ?x) (timepoint ?x))))
(=> (object ?x)
(not (timepoint ?x)))))
;;
;; Axiom 11 The occurrence relation only holds between activities and
;; activity occurrences.
;; (forall (?a ?occ) (=> (occurrence_of ?occ ?a) (and (activity ?a) (activity_occurrence ?occ)))) ;;;; Axiom 12 Every activity occurrence is the occurrence of some activity. ;;
(forall (?occ) (=> (activity_occurrence ?occ) (exists (?a) (and (activity ?a) (occurrence_of ?occ ?a))))) ;;;; Axiom 13 An activity occurrence is associated with a unique activity. ;;
(forall (?occ ?a1 ?a2)
(=> (and (occurrence_of ?occ ?a1)
(occurrence_of ?occ ?a2))
(equal ?a1 ?a2)))
;;
;; Axiom 14 The begin and end of an activity occurrence or object are timepoints.
;;
;;
(forall (?a ?x)
(=> (or (occurrence_of ?x ?a)
(object ?x))
(and (timepoint (beginof ?x))
(timepoint (endof ?x)))))
;;
;; Axiom 15 The begin point of every activity occurrence or object is
;; before or equal to its end point.
;; (forall (?x) (=> (or (activity_occurrence ?x) (object ?x)) (beforeEq (beginof ?x) (endof ?x)))) ;;;; Axiom 16 The participates_in relation only holds between objects, ;; activity occurrences, and timepoints, respectively. ;;
(forall (?x ?occ ?t) (=> (participates_in ?x ?occ ?t) (and (object ?x) (activity_occurrence ?occ) (timepoint ?t)))) ;;;; Axiom 17 An object can participate in an activity occurrence only at those timepoints ;; at which both the object exists and the activity is occurring. ;;
(forall (?x ?occ ?t)
(=> (participates_in ?x ?occ ?t)
(and (exists_at ?x ?t)
(is_occurring_at ?occ ?t))))
;;
;; (forall (?t1 ?t2 ?t3) (<=> (between ?t1 ?t2 ?t3) (and (before ?t1 ?t2) (before ?t2 ?t3)))) ;;;; Definition 2 Timepoint ?t1 is beforeEq timepoint ?t2 if and only if ?t1 is before or equal ;; to ?t2. ;;
(forall (?t1 ?t2) (<=> (beforeEq ?t1 ?t2)
(and (timepoint ?t1) (timepoint ?t2)
(or (before ?t1 ?t2) (equal ?t1 ?t2)))))
;;
;; Definition 3 Timepoint ?t2 is betweenEq timepoints ?t1 and ?t3 if and only if
;; ?t1 is before or equal to ?t2, and ?t2 is before or equal to ?t3.
;;
(forall (?t1 ?t2 ?t3) (<=> (betweenEq ?t1 ?t2 ?t3)
(and (beforeEq ?t1 ?t2)
(beforeEq ?t2 ?t3))))
;;
;; Definition 4 An object exists at a timepoint ?t if and only if ?t is betweenEq its begin
;; and end points.
;;
(forall (?x ?t) (<=> (exists_at ?x ?t)
(and (object ?x)
(betweenEq (beginof ?x) ?t (endof ?x)))))
;;
;; Definition 5 An activity is occurring at a timepoint ?t if and only if ?t
;; is betweenEq the begin and end points of the activity occurrence.
;; (forall (?occ ?t) (<=> (is_occurring_at ?occ ?t) (betweenEq (beginof ?occ) ?t (endof ?occ)))) ;;;;
;; ;;
;;;; Extension Name: act_occ.th
;; Primitive Lexicon: ;;
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?o1 ?o2) (=> (subactivity_occurrence ?o1 ?o2) (and (activity_occurrence ?o1) (activity_occurrence ?o2)))) ;;;; Axiom 1 ;; ;; There exists an occurrence of an activity ?a for every branch of an activity ;; tree for ?a. All atomic subactivity occurrences on the branch are subactivity ;; occurrences of the occurrence of ?a. ;; ;;
(forall (?a ?s1 ?s2) (=> (min_precedes ?s1 ?s2 ?a) (exists (?occ) (and (occurrence_of ?occ ?a) (subactivity_occurrence ?s1 ?occ) (subactivity_occurrence ?s2 ?occ))))) ;;;; Axiom 2 ;; ;; There exists an occurrence of an activity ?a for every branch of an activity ;; tree for ?a. All root subactivity occurrences on the branch are subactivity ;; occurrences of the occurrence of ?a. ;; ;;
(forall (?a ?s) (=> (root ?s ?a) (exists (?occ) (and (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ))))) ;;;; Axiom 3 ;; ;; Every occurrence of a complex activity a contains an atomic subactivity ;; occurrence that is the root of an activity tree for a. ;; ;;
(forall (?occ ?a)
(=> (and (occurrence_of ?occ ?a)
(not (atomic ?a)))
(exists (?s)
(and (root ?s ?a)
(subactivity_occurrence ?s ?occ)))))
;;
;; Axiom 4
;;
;; Distinct occurrences of an activity correspond to distinct branches of an activity tree.
;;
;; (forall (?a ?s1 ?occ1 ?occ2) (=> (and (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a) (not (atomic ?a)) (not (equal ?occ1 ?occ2)) (arboreal ?s1) (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s1 ?occ2)) (exists (?s2) (and (min_precedes ?s1 ?s2 ?a) (subactivity_occurrence ?s2 ?occ1) (not (subactivity_occurrence ?s2 ?occ2)))))) ;;;; Axiom 5 ;; ;; All atomic subactivity occurrences of a complex activity occurrence ;; are elements of the same branch of the activity tree. ;; ;;
(forall (?a ?occ ?s1 ?s2) (=> (and (occurrence_of ?occ ?a) (not (atomic ?a)) (arboreal ?s1) (arboreal ?s2) (subactivity_occurrence ?s1 ?occ) (subactivity_occurrence ?s2 ?occ)) (or (min_precedes ?s1 ?s2 ?a) (min_precedes ?s2 ?s1 ?a) (equal ?s1 ?s2)))) ;;;; Axiom 6 ;; All elements of the same branch of an activity tree are atomic ;; subactivity occurrences of the same activity occurrences. ;;
(forall (?a ?s1 ?s2 ?occ) (=> (and (min_precedes ?s1 ?s2 ?a) (subactivity_occurrence ?s2 ?occ)) (subactivity_occurrence ?s1 ?occ))) ;;;; Axiom 7 ;; The subactivity_occurrence relation preserves the subactivity relation. ;;
(forall (?a1 ?a2 ?occ1 ?occ2) (=> (and (occurrence_of ?occ1 ?a1) (occurrence_of ?occ2 ?a2) (subactivity_occurrence ?occ1 ?occ2)) (subactivity ?a1 ?a2))) ;;;; Axiom 8 ;; The subactivity_occurrence relation is transitive. ;;
(forall (?occ1 ?occ2 ?occ3)
(=> (and (subactivity_occurrence ?occ1 ?occ2)
(subactivity_occurrence ?occ2 ?occ3))
(subactivity_occurrence ?occ1 ?occ3)))
;;
;; Axiom 9
;; Occurrences of subactivities are subactivity occurrences if the
;; occurrences satisfy branch containment.
;;
(forall (?a1 ?a2 ?occ1 ?occ2)
(=> (and (occurrence_of ?occ1 ?a1)
(occurrence_of ?occ2 ?a2)
(subactivity ?a1 ?a2)
(not (subactivity_occurrence ?occ1 ?occ2)))
(exists (?s)
(and (subactivity_occurrence ?s ?occ2)
(not (subactivity_occurrence ?s ?occ1))))))
;;
;; Axiom 10
;; The beginof timepoint for a complex activity occurrence is
;; equal to the beginof timepoint of its root occurrence.
;; (forall (?occ) (=> (activity_occurrence ?occ) (equal (beginof ?occ) (beginof (root_occ ?occ))))) ;;;; Axiom 11 ;; The endof timepoint for a complex activity occurrence is ;; equal to the endof timepoint of its leaf occurrence. ;;
(forall (?s ?occ) (=> (leaf_occ ?s ?occ) (equal (endof ?occ) (endof ?s)))) ;;;; Axiom 12 ;; ;; The mono relation is a branch homomorphism. ;; ;;
(forall (?s1 ?s2 ?a)
(=> (mono ?s1 ?s2 ?a)
(hom ?s1 ?s2 ?a)))
;;
;; Axiom 13
;;
;; If an atomic subactivity occurrence is mapped in a branch homomorphism,
;; then there exists another atomic subactivity occurrence that is mono with it.
;;
;;
(forall (?s1 ?s2 ?a)
(=> (and (hom ?s1 ?s2 ?a)
(not (mono ?s1 ?s2 ?a)))
(exists (?s3)
(or (and (min_precedes ?s3 ?s2 ?a)
(mono ?s1 ?s3 ?a))
(and (min_precedes ?s3 ?s1 ?a)
(mono ?s2 ?s3 ?a))))))
;;
;; Axiom 14
;;
;; The mono relation is restricted to one-to-one homomorphisms between different
;; branches of the activity tree.
;;
;;
(forall (?s1 ?s2 ?s3 ?a)
(=> (and (mono ?s1 ?s2 ?a)
(mono ?s3 ?s2 ?a))
(not (or (min_precedes ?s1 ?s3 ?a)
(min_precedes ?s3 ?s1 ?a)))))
;;
;; Axiom 15
;;
;; The mono relation is symmetric on activity occurrences.
;;
;;
(forall (?s1 ?s2 ?a)
(=> (mono ?s1 ?s2 ?a)
(mono ?s2 ?s1 ?a)))
;;
;; Axiom 16
;;
;; The mono relation is transitive on activity occurrences.
;;
;;
(forall (?s1 ?s2 ?s3 ?a)
(=> (and (mono ?s1 ?s2 ?a)
(mono ?s2 ?s3 ?a))
(mono ?s1 ?s3 ?a)))
;;
;;
(forall (?s1 ?s2 ?a) (<=> (iso_occ ?s1 ?s2 ?a)
(exists (?a1 ?a2 ?a3)
(and (atomic ?a1)
(atomic ?a2)
(atomic ?a3)
(subactivity ?a1 ?a)
(occurrence_of ?s1 (conc ?a1 ?a2))
(occurrence_of ?s2 (conc ?a1 ?a3))))))
;;
;; Definition 2
;;
;; For every two occurrences of the same activity on different branches of an
;; activity tree, there exist homomorphic occurrences on those branches.
;;
;; (forall (?s1 ?s2 ?a) (<=> (hom ?s1 ?s2 ?a) (exists (?occ1 ?occ2) (and (iso_occ ?s1 ?s2 ?a) (not (min_precedes ?s1 ?s2 ?a)) (not (min_precedes ?s2 ?s1 ?a)) (subactivity_occurrence ?s1 ?occ1) (subactivity_occurrence ?s2 ?occ2) (occurrence_of ?occ1 ?a) (occurrence_of ?occ2 ?a))))) ;;;; Definition 3 ;; An occurrence ?occ1 is the root occurrence of an occurrence of ?a if and only if ;; it is a subactivity occurrence and it is the root of an activity tree for ?a. ;; ;;
(forall (?s ?occ)
(=> (and (activity_occurrence ?s)
(activity_occurrence ?occ))
(<=> (equal ?s (root_occ ?occ))
(exists (?a)
(and (occurrence_of ?occ ?a)
(subactivity_occurrence ?s ?occ)
(root ?s ?a))))))
;;
;; Definition 4
;; An occurrence ?occ1 is the leaf occurrence of an occurrence of ?a if and only if
;; it is a subactivity occurrence and it is the leaf of an activity tree for ?a.
;;
;; (forall (?s ?occ) (<=> (leaf_occ ?s ?occ) (exists (?a) (and (occurrence_of ?occ ?a) (subactivity_occurrence ?s ?occ) (leaf ?s ?a))))) ;;;; Definition 5 ;; Two complex activity occurrences are in the same grove ;; iff they are occurrences of the same activity and their ;; root occurrences are siblings. ;;
(forall (?occ1 ?occ2) (<=> (same_grove ?occ1 ?occ2)
(exists (?a)
(and (occurrence_of ?occ1 ?a)
(occurrence_of ?occ2 ?a)
(or (and (initial (root_occ ?occ1))
(initial (root_occ ?occ2)))
(exists (?s4 ?a1 ?a2)
(and (equal (root_occ ?occ1) (successor ?a1 ?s4))
(equal (root_occ ?occ2) (successor ?a2 ?s4)))))))))
;;
;;
;;
;;
;; ;;
;;
;; (subactivity_occurrence ?occ1 ?occ2) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if the branch corresponding to the activity occurrence ?occ1 is a subset of the branch corresponding to activity occurrence ?occ2. ;;
;; (root_occ ?occ1 ?occ2) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if activity occurrence ?occ1 is the root occurrence in the branch of the activity tree for ?a corresponding to the activity occurrence ?occ2. ;;
;; (leaf_occ ?occ1 ?occ2) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if activity occurrence ?occ1 is the leaf occurrence in the branch of the activity tree for ?a corresponding to the activity occurrence ?occ2. ;;
;; (iso_occ ?occ1 ?occ2 ?a) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if both ?occ1 and ?occ2 are occurrences of an atomic activity that contain a common subactivity. ;;
;; (same_grove ?occ1 ?occ2) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if activity occurrences ?occ1 and ?occ2 of ?a correspond to branches in the same activity tree for ?a. ;;
;; (mono ?s1 ?s2 ?a) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if ;; there is a one-to-one mapping between branches of an activity tree for ?a that ;; maps the atomic subactivity occurrence ?s1 to the atomic subactivity occurrence ;; ?s2. ;;
;; (hom ?s1 ?s2 ?a) ;; is TRUE in an interpretation of the Activity Occurrence Theory if and only if ;; there is a mapping between branches of an activity tree for ?a that ;; maps the atomic subactivity occurrence ?s1 to the atomic subactivity occurrence ;; ?s2. ;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: atomic.th
;; Primitive Lexicon:
;; Relations: ;;
;; Theories Required by this Extension: occtree.th,subactivity.th, psl_core.th
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?a) (=> (primitive ?a) (atomic ?a))) ;;;; Axiom 2 The function conc is idempotent. ;;
(forall (?a) (equal ?a (conc ?a ?a))) ;;;; Axiom 3 The function conc is commutative. ;;
(forall (?a1 ?a2) (equal (conc ?a1 ?a2) (conc ?a2 ?a1))) ;;;; Axiom 4 The function conc is associative. ;;
(forall (?a1 ?a2 ?a3) (equal (conc ?a1 (conc ?a2 ?a3)) (conc (conc ?a1 ?a2) ?a3))) ;;;; Axiom 5 The concurrent aggregation of atomic action is an atomic action. ;; ;;
(forall (?a1 ?a2) (<=> (atomic (conc ?a1 ?a2)) (and (atomic ?a1) (atomic ?a2)))) ;;;; Axiom 6 An atomic activity ?a1 is a subactivity of an atomic activity ?a2 if and only if ;; ?a2 is an idempotent for ?a1. ;;
(forall (?a1 ?a2) (=> (and (atomic ?a1) (atomic ?a2)) (<=> (subactivity ?a1 ?a2) (equal ?a2 (conc ?a1 ?a2))))) ;;;; Axiom 7 An atomic action has a proper subactivity if and only if there exists another atomic ;; activity which can be concurrently aggregated. ;;
(forall (?a1 ?a2) (=> (and (atomic ?a2) (subactivity ?a1 ?a2) (not (equal ?a1 ?a2))) (exists (?a3) (and (atomic ?a3) (equal ?a2 (conc ?a1 ?a3)) (not (exists (?a4) (and (atomic ?a4) (subactivity ?a4 ?a1) (subactivity ?a4 ?a3)))))))) ;;;; Axiom 8 The semilattice of atomic activities is distributive. ;;
(forall (?a ?b0 ?b1) (=> (and (atomic ?a) (atomic ?b0) (atomic ?b1) (subactivity ?a (conc ?b0 ?b1)) (not (primitive ?a))) (exists (?a0 ?a1) (and (subactivity ?a0 ?a) (subactivity ?a1 ?a) (equal ?a (conc ?a0 ?a1)))))) ;;;; Axiom 9 ;; Only atomic activities can be generator activities. ;; Equivalently, only occurrences of atomic activities can be ;; elements of an occurrence tree. ;; ;;
(forall (?a) (=> (generator ?a) (atomic ?a))) ;;;; Axiom 10 ;; Atomic activities are activities. ;; ;;
(forall (?a) (=> (atomic ?a) (activity ?a))) ;;;;
;; ;; ;;
;;;; Although the Subactivity Theory can represent arbitrary composition of activities, ;; the composition of atomic activities is restricted to concurrency; ;; to represent complex, or nonatomic, activities requires the Complex Activity Theory. ;;
;; The basic ontological commitments of the Atomic Activity Theory are based on the ;; following intuitions: ;;
;; Intuition 1: ;;
;; ;; Concurrency is represented by the occurrence of one concurrent activity ;; rather than multiple concurrent occurrences. ;; ;;
;; Since concurrent activities may have preconditions and effects that are not ;; the conjunction of the preconditions and effects of their activities, ;; this core theory takes the following approach: ;;
;; Intuition 2: ;;
;; ;; Every concurrent activity is equivalent to the composition of a set of ;; primitive activities. ;; ;;
;; Atomic activities are either primitive or concurrent (in which case they ;; have proper subactivities). ;; The Atomic Activities core theory introduces the function conc that ;; maps any two atomic activities to the activity that is their concurrent composition. ;; Essentially, what we call an atomic activity corresponds to some set of primitive ;; activities. ;;
;;
;; (atomic ?a) is TRUE in an interpretation of the Atomic Activity ;; Theory if and only if either ?a is primitive or it is the concurrent superposition ;; of a set of primitive activities. ;;
;; (equal ?a (conc ?a1 ?a2)) is TRUE in an interpretation of the ;; Atomic Activity Theory if and only if ;; ?a3 is the atomic activity that is the concurrent superposition of the two atomic ;; activities ?a1 and ?a2. ;;
;; (primitive ?a) is TRUE in an interpretation of the Atomic Activity ;; if and only if ?a has no proper subactivities. ;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: complex.th
;; Primitive Lexicon: ;;
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?a ?s1 ?s2) (=> (min_precedes ?s1 ?s2 ?a) (exists (?a1 ?a2) (and (subactivity ?a1 ?a) (atomic ?a2) (subactivity ?a1 ?a2) (occurrence_of ?s1 ?a2))))) ;;;; Axiom 2 ;; Occurrences in the activity tree for an activity correspond to atomic subactivity ;; occurrences of the activity. ;;
(forall (?a ?s1 ?s2) (=> (min_precedes ?s1 ?s2 ?a) (exists (?a2 ?a3) (and (subactivity ?a2 ?a) (atomic ?a3) (subactivity ?a2 ?a3) (occurrence_of ?s2 ?a3))))) ;;;; Axiom 3 ;; Root occurrences in the activity tree correspond to atomic subactivity ;; occurrences of the activity. ;;
(forall (?a ?s) (=> (root ?s ?a) (exists (?a2 ?a3) (and (subactivity ?a2 ?a3) (atomic ?a3) (subactivity ?a2 ?a) (occurrence_of ?s ?a3))))) ;;;; Axiom 4 ;; All activity trees have a root subactivity occurrence. ;;
(forall (?s1 ?s2 ?a) (=> (min_precedes ?s1 ?s2 ?a) (exists (?s3) (and (root ?s3 ?a) (or (min_precedes ?s3 ?s1 ?a) (equal ?s3 ?s1)))))) ;;;; Axiom 5 ;; No subactivity occurrences in an activity tree occur earlier than ;; the root subactivity occurrence. ;;
(forall (?s ?a) (=> (root ?s ?a) (not (exists (?s2) (and (activity_occurrence ?s2) (min_precedes ?s2 ?s ?a)))))) ;;;; Axiom 6 ;; An activity tree is a subtree of the occurrence tree. ;;
(forall (?s1 ?s2 ?a) (=> (min_precedes ?s1 ?s2 ?a) (precedes ?s1 ?s2))) ;;;; Axiom 7 ;; Root occurrences are elements of the occurrence tree. ;;
(forall (?s ?a) (=> (root ?s ?a) (legal ?s))) ;;;; Axiom 8 ;; Every legal atomic activity occurrence is an activity tree containing only ;; one occurrence. ;;
(forall (?a1 ?a2 ?s)
(=> (and (atomic ?a1)
(occurrence_of ?s ?a1)
(legal ?s)
(subactivity ?a2 ?a1))
(root ?s ?a2)))
;;
;; Axiom 9
;; Activity trees are discrete.
;; (forall (?a ?s1 ?s2) (=> (min_precedes ?s1 ?s2 ?a) (exists (?s3) (and (next_subocc ?s1 ?s3 ?a) (or (min_precedes ?s3 ?s2 ?a) (equal ?s3 ?s2)))))) ;;;; Axiom 10 ;; Subactivity occurrences on the same branch of the occurrence tree are ;; on the same branch of the activity tree. ;;
(forall (?a ?s1 ?s2 ?s3) (=> (and (min_precedes ?s1 ?s2 ?a) (min_precedes ?s1 ?s3 ?a) (precedes ?s2 ?s3)) (min_precedes ?s2 ?s3 ?a))) ;;;; Axiom 11 ;; The activity tree for a complex subactivity occurrence ;; is a subtree of the activity tree for the activity occurrence. ;;
(forall (?a1 ?a2) (=> (subactivity ?a1 ?a2) (not (exists (?s) (and (activity_occurrence ?s) (subtree ?s ?a2 ?a1)))))) ;;;; Axiom 12 ;; Only complex activities can be arguments to the min_precedes relation. ;;
(forall (?s1 ?s2 ?a)
(=> (min_precedes ?s1 ?s2 ?a)
(not (atomic ?a))))
;;
;; Axiom 13
;; Subactivity occurrences on the same branch of the activity tree are
;; linearly ordered by the min_precedes relation.
;; (forall (?a ?s1 ?s2 ?s3) (=> (and (min_precedes ?s2 ?s1 ?a) (min_precedes ?s3 ?s1 ?a) (precedes ?s2 ?s3)) (min_precedes ?s2 ?s3 ?a))) ;;;;
(forall (?s ?a) (<=> (leaf ?s ?a) (exists (?s1) (and (arboreal ?s1) (or (root ?s ?a) (min_precedes ?s1 ?s ?a)) (not (exists (?s2) (min_precedes ?s ?s2 ?a))))))) ;;;; Definition 2 ;; The do relation specifies the initial and final atomic subactivity occurrences ;; of an occurrence of an activity. ;;
(forall (?a ?s1 ?s2) (<=> (do ?a ?s1 ?s2) (and (root ?s1 ?a) (leaf ?s2 ?a) (or (min_precedes ?s1 ?s2 ?a) (equal ?s1 ?s2))))) ;;;; Definition 3 ;; An activity occurrence ?s2 is the next subactivity occurrence after ?s1 ;; in an activity tree for ?a if and only of ?s1 precedes ?s2 ;; in the tree and there does not exist a subactivity occurrence that is between ;; them in the tree. ;;
(forall (?s1 ?s2 ?a) (<=> (next_subocc ?s1 ?s2 ?a)
(and (min_precedes ?s1 ?s2 ?a)
(not (exists (?s3)
(and (activity_occurrence ?s3)
(min_precedes ?s1 ?s3 ?a)
(min_precedes ?s3 ?s2 ?a)))))))
;;
;; Definition 4
;; The activity tree for ?a1 with root occurrence ?s1
;; contains an activity tree for ?a2 as a subtree if and only if
;; every atomic subactivity occurrence in the activity tree for ?a2
;; is an element of the activity tree for ?a1, and there is an atomic subactivity
;; occurrence in the activity tree for ?a1 that is not in the activity tree for ?a2.
;;
;;
(forall (?s1 ?a1 ?a2) (<=> (subtree ?s1 ?a1 ?a2)
(and (root ?s1 ?a1)
(exists (?s2 ?s3)
(and (root ?s2 ?a2)
(min_precedes ?s1 ?s2 ?a1)
(min_precedes ?s1 ?s3 ?a1)
(not (min_precedes ?s2 ?s3 ?a2)))))))
;;
;; Definition 5
;;
;; The atomic subactivity occurrences ?s1 and ?s2 are siblings
;; in an activity tree for ?a iff they either have a common
;; predecessor in the activity tree or they are both roots of
;; activity trees that have a common predecessor in the occurrence
;; tree.
;;
;; (forall (?s1 ?s2 ?a) (<=> (sibling ?s1 ?s2 ?a) (or (exists (?s3) (and (next_subocc ?s3 ?s1 ?a) (next_subocc ?s3 ?s2 ?a))) (and (root ?s1 ?a) (root ?s2 ?a) (or (and (initial ?s1) (initial ?s2)) (exists (?s4 ?a1 ?a2) (and (equal ?s1 (successor ?a1 ?s4)) (equal ?s2 (successor ?a2 ?s4))))))))) ;;;;
;; ;; ;;
;;;;
;; The basic ontological commitments of the Complex Activities Theory are based on the ;; following intuitions: ;;
;; Intuition 1: ;;
;; ;; An activity tree consists of all possible sequences ;; of atomic subactivity occurrences beginning from a root subactivity occurrence. ;; ;;
;; In a sense, activity trees are a microcosm of the occurrence tree, in which ;; we consider all of the ways in which the world unfolds in the context of ;; an occurrence of the complex activity. ;;
;; Any activity tree is actually ;; isomorphic to multiple copies of a minimal activity tree arising from the fact ;; that other external activities may be occurring during the complex activity. ;;
;; Intuition 2: ;;
;; ;; Different subactivities may occur on different branches of the activity tree i.e. ;; different occurrences of an activity may have different subactivity occurrences ;; or different orderings on the same subactivity occurrences. ;; ;;
;; In this sense, branches of the activity tree characterize the nondeterminism that ;; arises from different ordering constraints or iteration. ;;
;; Intuition 3: ;;
;; ;; An activity will in general have multiple activity trees within an occurrence ;; tree, and not all activity trees for an activity need be isomorphic. ;; Different activity trees for the same activity can have different subactivity ;; occurrences. ;; ;;
;; Following this intuition, ;; the Complex Activities Theory does not constrain which subactivities occur. ;; For example, conditional activities are characterized by cases in which the state ;; that holds prior to the activity occurrence determines which subactivities occur. ;; In fact, an activity may have subactivities that do not occur; the only constraint ;; is that any subactivity occurrence must correspond to a subtree of the activity tree ;; that characterizes the occurrence of the activity. ;;
;; Intuition 4: ;;
;; ;; Not every occurrence of a subactivity is a subactivity occurrence. There may ;; be other external activities that occur during an occurrence of an activity. ;; ;;
;; This theory does not force the existence of complex activities; ;; there may be subtrees of the occurrence tree that contain occurrences of subactivities, ;; yet not be activity trees. ;; This allows for the existence of activity attempts, intended effects, and temporal ;; constraints; subtrees that do not satisfy the desired constraints will simply not ;; correspond to activity trees for the activity. ;;
;;
;; (min_precedes ?s1 ?s2 ?a) is TRUE in an interpretation of the ;; Complex Activity Theory if and only if ?s1 and ?s2 are subactivity occurrences ;; in the activity tree for ?a, and ?s1 precedes ?s2 in the subtree. ;; Any occurrence of an activity ?a corresponds to an activity tree (which is a subtree ;; of the occurrence tree). The activity occurrences within this subtree are the ;; subactivity occurrences of the occurrence of ?a. ;;
;; (root ?s ?a) is TRUE in an interpretation of the Complex Activity ;; Theory if and only if the activity occurrence ?s is the root of an activity tree for ?a. ;;
;; (subtree ?a1 ?a2) ?occ2) is TRUE in an interpretation of the Complex ;; Activity Theory if and only if every atomic subactivity occurrence in the activity ;; tree for ?a1 is an element of the activity tree for ?a2. ;;
;; (do ?a ?s1 ?s2) is TRUE in an interpretation of the Complex ;; Activity Theory if and only if ?s1 is the root of an activity tree and ?s2 ;; is a leaf of the same activity tree such that both activity occurrences are ;; elements of the same branch of the activity tree. ;;
;; (leaf ?s ?a) is TRUE in an interpretation of the Complex Activity ;; Theory if and only if the activity occurrence ?s is the leaf of an activity tree for ?a. ;;
;; (next_subocc ?s1 ?s2 ?a) is TRUE in an interpretation of the ;; Complex Activity Theory if and only if ?s1 precedes ?s2 in the tree and there does ;; not exist a subactivity occurrence that is between them in the tree. ;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: disc_state.th
;; Primitive Lexicon:
;; Relations: ;;
;; Theories Required by this Extension: occtree.th, psl_core.th
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?f) (=> (state ?f) (object ?f))) ;;;; Axiom 2 ;; The holds relation is only between states and arboreal ctivity occurrences. ;; Intuitively, it means that the fluent (property of the world) is true after ;; the activity occurrence ?occ. ;;
(forall (?f ?occ) (=> (holds ?f ?occ) (and (state ?f) (arboreal ?occ)))) ;;;; Axiom 3 ;; The prior relation is only between states and arboreal activity occurrences. ;; Intuitively, it means that the fluent (property of the world) is true before ;; the activity occurrence ?occ. ;;
(forall (?f ?occ) (=> (prior ?f ?occ) (and (state ?f) (arboreal ?occ)))) ;;;; Axiom 4 ;; All initial occurrences agree on the states that hold prior to them. ;;
(forall (?occ1 ?occ2 ?f) (=> (and (initial ?occ1) (initial ?occ2)) (<=> (prior ?f ?occ1) (prior ?f ?occ2)))) ;;;; Axiom 5 ;; A state holds after an arboreal activity occurrence if and only if it ;; holds prior to the successor occurrence. ;;
(forall (?f ?a ?occ)
(<=> (prior ?f (successor ?a ?occ))
(and (holds ?f ?occ)
(generator ?a))))
;;
;; Axiom 6
;; If a fluent holds after some activity occurrence, then there exists
;; an earliest activity occurrence along the branch where the fluent holds.
;;
;; (forall (?occ1 ?f) (=> (holds ?f ?occ1) (exists (?occ2) (and (earlierEq ?occ2 ?occ1) (holds ?f ?occ2) (or (initial ?occ2) (not (prior ?f ?occ2))) (forall (?occ3) (=> (and (earlier ?occ2 ?occ3) (earlier ?occ3 ?occ1)) (holds ?f ?occ3))))))) ;;;; Axiom 7 ;; If a fluent does not hold after some activity occurrence, then there exists ;; an earliest activity occurrence along the branch where the fluent does not hold. ;; ;;
(forall (?occ1 ?f) (=> (and (state ?f) (arboreal ?occ1) (not (holds ?f ?occ1))) (exists (?occ2) (and (earlierEq ?occ2 ?occ1) (not (holds ?f ?occ2)) (or (initial ?occ2) (prior ?f ?occ2)) (not (exists (?occ3) (and (earlier ?occ2 ?occ3) (earlier ?occ3 ?occ1) (holds ?f ?occ3)))))))) ;;;; Axiom 8 ;; ;; If a fluent holds, there exists an earliest activity occurrence where it ;; holds. ;; ;;
(forall (?f ?s1) (=> (holds ?f ?s1) (exists (?s2) (and (holds ?f ?s2) (earlierEq ?s2 ?s1) (forall (?s3) (=> (holds ?f ?s3) (not (earlier ?s3 ?s2)))))))) ;;;;
;; ;; ;;
;;;; The definitional extensions of this theory ;; use different constraints on possible activity occurrences ;; as a way of classifying activities with respect to preconditions and effects. ;;
;; The basic ontological commitments of the Discrete State Theory are based on the ;; following intuitions: ;;
;; Intuition 1: ;;
;; ;; State is changed by the occurrence of activities. ;; ;;
;; Intuitively, a change in state is captured by a state that ;; is either achieved or falsified by an activity occurrence. ;; We therefore need a relation that specifies the state that is ;; intuitively true prior to an activity occurrence and also a ;; relation that specifies the state that is ;; intuitively true after an activity occurrence. ;;
;; Intuition 2: ;;
;; ;; State can only be changed by the occurrence of activities. ;; ;;
;; Thus, if some state holds after an activity occurrence, ;; but after an activity occurrence later along the branch it is false, ;; then an activity must occur at some point between that changes the state. ;; This also leads to the requirement ;; that the state holding after an activity occurrence will be the same ;; state holding prior to any immediately succeeding occurrence, since ;; there cannot be an activity occurring between the two by definition. ;;
;; Intuition 3: ;;
;; ;; State does not change during the occurrence of an activity in the ;; occurrence tree. ;; ;;
;; The Discrete State Theory cannot represent phenomena in which ;; some feature of the world is changing as some continuous function of ;; time (hence the name "Discrete State" for the extension). ;; State can change during an activity occurrence only if the activity is complex. ;;
;;
;; (state ?f) is TRUE in an interpretation of the Discrete State Theory ;; if and only if ?f is a member of the set of states in the universe of discourse of ;; the interpretation. States are a subcategory of object. ;; They intuitively represent properties and relationships in the domain that can change ;; as the result of the occurrence of activities. ;;
;; (holds ?f ?occ) is TRUE in an interpretation of the Discrete ;; State Theory if and only if the state ?f is true after the activity occurrence ?occ. ;;
;; (prior ?f ?occ) is TRUE in an interpretation of the Discrete State ;; Theory if and only if the state ?f is true prior to the activity occurrence ?occ. ;;
;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: occtree.th
;; Primitive Lexicon:
;; Relations: ;;
;; Relations: ;;
;; Theories Required by this Extension: psl_core.th
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?s1 ?s2) (=> (earlier ?s1 ?s2) (and (arboreal ?s1) (arboreal ?s2)))) ;;;; Axiom 2 The ordering relation over occurrences is irreflexive. ;;
(forall (?s1 ?s2) (=> (earlier ?s1 ?s2) (not (earlier ?s2 ?s1)))) ;;;; Axiom 3 The ordering relation over occurrences is transitive. ;;
(forall (?s1 ?s2 ?s3) (=> (and (earlier ?s1 ?s2) (earlier ?s2 ?s3)) (earlier ?s1 ?s3))) ;;;; Axiom 4 A branch in the occurrence tree is totally ordered. ;;
(forall (?s1 ?s2 ?s3) (=> (and (earlier ?s1 ?s2) (earlier ?s3 ?s2)) (or (earlier ?s1 ?s3) (earlier ?s3 ?s1) (equal ?s3 ?s1)))) ;;;; Axiom 5 No occurrence in the occurrence tree is earlier than an initial occurrence. ;;
(forall (?s) (<=> (initial ?s) (and (arboreal ?s) (not (exists (?sp) (earlier ?sp ?s)))))) ;;;; Axiom 6 Every branch of the occurrence tree has an initial occurrence. ;;
(forall (?s1 ?s2) (=> (earlier ?s1 ?s2) (exists (?sp) (and (initial ?sp) (earlierEq ?sp ?s1))))) ;;;; Axiom 7 There is an initial occurrence of each activity. ;;
(forall (?s ?a)
(=> (occurrence_of ?s ?a)
(<=> (arboreal ?s)
(generator ?a))))
;;
;; Axiom 8
;; No two initial activity occurrences in the occurrence tree are occurrences
;; of the same activity.
;; (forall (?s1 ?s2 ?a) (=> (and (initial ?s1) (initial ?s2) (occurrence_of ?s1 ?a) (occurrence_of ?s2 ?a)) (equal ?s1 ?s2))) ;;;; Axiom 9 The successor of an arboreal activity occurrence is an occurrence of a generator activity. ;;
(forall (?a ?o)
(<=> (occurrence_of (successor ?a ?o) ?a)
(and (generator ?a)
(arboreal ?o))))
;;
;; Axiom 10 Every non-initial activity occurrence is the successor of
;; another activity occurrence.
;;
(forall (?s1 ?s2)
(=> (earlier ?s1 ?s2)
(exists (?a ?s3)
(and (generator ?a)
(equal ?s2 (successor ?a ?s3))))))
;;
;; Axiom 11 An occurrence ?s1 is earlier than the successor occurrence
;; of ?s2 if and only if the occurrence ?s2 is later than ?s1.
;;
(forall (?a ?s1 ?s2)
(=> (generator ?a)
(<=> (earlier ?s1 (successor ?a ?s2))
(earlierEq ?s1 ?s2))))
;;
;; Axiom 12 The legal relation restricts arboreal activity occurrences.
;; (forall (?s) (=> (legal ?s) (arboreal ?s))) ;;;; Axiom 13 If an activity occurrence is legal, all earlier activity ;; occurrences in the occurrence tree are also legal. ;;
(forall (?s1 ?s2) (=> (and (legal ?s1) (earlier ?s2 ?s1)) (legal ?s2))) ;;;; Axiom 14 The endof an activity occurrence is before to the beginof ;; the successor of the activity occurrence. ;;
(forall (?s1 ?s2) (=> (earlier ?s1 ?s2) (before (endof ?s1) (beginof ?s2)))) ;;;;
(forall (?s1 ?s2) (<=> (precedes ?s1 ?s2) (and (earlier ?s1 ?s2) (legal ?s2)))) ;;;; Definition 2 An activity occurrence ?s1 is EarlierEq than ;; an activity occurrence ?s2 if and only if it is either earlier than ;; ?s2 or it is equal to ?s2. ;;
(forall (?s1 ?s2) (<=> (earlierEq ?s1 ?s2) (and (arboreal ?s1) (arboreal ?s2) (or (earlier ?s1 ?s2) (equal ?s1 ?s2))))) ;;;; Definition 3 ;; ;; An activity is poss at some occurrence if and only if the successor ;; occurrence of the activity is legal. ;; ;;
(forall (?a ?s) (<=> (poss ?a ?s) (legal (successor ?a ?s)))) ;;;; Definition 4 ;; ;; An activity is a generator iff it has an initial occurrence in the ;; occurrence tree. ;; ;; ;;
(forall (?a) (<=> (generator ?a)
(exists (?s)
(and (initial ?s)
(occurrence_of ?s ?a)))))
;; ;;
;; Definition 5
;;
;; An activity occurrence is arboreal iff it is an element of an occurrence tree.
;;
;; ;;
(forall (?s) (<=> (arboreal ?s)
(exists (?sp)
(earlier ?s ?sp))))
;; ;;
;; ;; ;; ;;
;;;; It should be noted that the occurrence tree is not the structure that represents the ;; occurrences of subactivities of an activity. The occurrence tree is not representing ;; a particular occurrence of an activity, but rather all possible occurrences of all ;; activities in the domain. ;;
;; The basic ontological commitments of the Occurrence Tree Theory are based on the ;; following intuitions: ;;
;; Intuition 1: ;;
;; ;; An occurrence tree is a partially ordered set of activity occurrences, ;; such that for a given set of activities, all discrete sequences of their occurrences ;; are branches of the tree. ;; ;;
;; An occurrence tree contains all occurrences of all activities; it is ;; not simply the set of occurrences of a particular (possibly complex) activity. ;; Because the tree is discrete, each activity occurrence in the tree has a unique ;; successor occurrence of each activity. ;;
;; Intuition 2: ;;
;; ;; There are constraints on which activities can possibly occur in some domain. ;; ;;
;; This intuition is the cornerstone for characterizing the semantics of classes of ;; activities and process descriptions. ;; Although occurrence trees characterize all sequences of activity occurrences, ;; not all of these sequences will intuitively be physically possible within the ;; domain. We will therefore want to consider the subtree of the occurrence ;; tree that consists only of possible sequences of activity occurrences; ;; this subtree is referred to as the legal occurrence tree. ;;
;; The definitional extensions of the PSL Ontology ;; use different constraints on possible activity occurrences ;; as a way of classifying activities. ;;
;; Intuition 3: ;;
;; ;; Every sequence of activity occurrences has an initial occurrence (which is the ;; root of an occurrence tree). ;; ;;
;; This intuition is closely related to the properties of occurrence trees. ;; For example, one could consider occurrences to form a semilinear ordering ;; (which need not have a root element) rather than a tree (which must have a root ;; element). ;; However, we are using occurrence trees to characterize the semantics of ;; different classes of activities, rather than using the occurrence tree ;; to represent history (which may not have an explicit initial event). ;; In our case, it is sufficient to consider all possible interactions between ;; the set of activities in the domain, and ;; we lose nothing by restricting our attention ;; to initial occurrences of the activities. ;; For example, given the query "Can the factory produce 1000 widgets by Friday?", ;; one can take the initial state to be the current state, and the initial activity ;; occurrences being the activities that could be performed at the current time. ;;
;; Intuition 4: ;;
;; ;; The ordering of activity occurrences in a branch of an occurrence tree ;; respects the temporal ordering. ;; ;;
;; Within the theory of occurrence trees, the ordering over ;; activity occurrences and the ordering over timepoints are distinct. ;; The set of activity occurrences ;; is partially ordered (hence the intuition about occurrence trees), but ;; timepoints are linearly ordered (since this theory is an extension of PSL-Core). ;; However, every branch of an occurrence tree is totally ordered, and the intuition ;; requires that the beginof timepoint for an activity occurrence along a branch is ;; before the beginof timepoints of all following activity occurrences on that branch. ;;
;;
;; (initial ?occ) is TRUE in an interpretation of the Occurrence Tree ;; Theory if and only if the activity occurrence ?occ is a root of the occurrence tree. ;;
;; (earlier ?occ1 ?occ2) is TRUE in an interpretation of the ;; Occurrence Tree Theory if and only if the two activity occurrences ?occ1 and ?occ2 ;; are on the same branch of the tree and ?occ1 is closer to the root of the ;; tree than ?occ2. ;; In other words, the earlier relation specifies the partial ordering ;; over the activity occurrences in this tree. ;;
;; (= (successor ?a ?occ) ?occ2) is TRUE in an interpretation of the ;; Occurrence Tree Theory if and only if ?occ2 denotes the occurrence of ?a that ;; follows consecutively after the activity occurrence ?occ in the occurrence tree. ;;
;; (arboreal ?s) is TRUE in an interpretation of the Occurrence ;; Tree Theory if and only if ?s is an element of the occurrence tree. ;;
;; (generator ?a) is TRUE in an interpretation of the Occurrence ;; Tree Theory if and only if ?a is an activity whose occurrences are ;; elements of the occurrence tree. ;;
;; (legal ?occ) is TRUE in an interpretation of the ;; Occurrence Tree Theory if and only if the activity occurrence ?occ is ;; an element of the legal occurrence tree. ;;
;; (poss ?a ?occ) is TRUE in an interpretation of the Occurrence ;; Tree Theory if and only if the activity ?a can possibly occur after the ;; activity occurrence ?occ. ;;
;; (precedes ?occ1 ?occ2) is TRUE in an interpretation of the ;; Occurrence Tree Theory if and only if the activity occurrence ?occ1 is earlier ;; than the activity occurrence ?occ2 in the occurrence tree and such that all ;; activity occurrences between them correspond to activities that are possible. ;; This relation specfies the sub-tree of the occurrence tree in which every activity ;; occurrence is the occurrence of an activity that is possible ;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: subactivity.th
;; Primitive Lexicon:
;; Relations: ;;
;; Relations: ;;
;; Theories Required by this Extension: psl_core.th
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?a1 ?a2) (=> (subactivity ?a1 ?a2) (and (activity ?a1) (activity ?a2)))) ;;;; Axiom 2 The subactivity relation is reflexive. ;;
(forall (?a) (=> (activity ?a) (subactivity ?a ?a))) ;;;; Axiom 3 The subactivity relation is antisymmetric. ;;
(forall (?a1 ?a2) (=> (and (subactivity ?a1 ?a2) (subactivity ?a2 ?a1)) (equal ?a1 ?a2))) ;;;; Axiom 4 The subactivity relation is transitive. ;;
(forall (?a1 ?a2 ?a3) (=> (and (subactivity ?a1 ?a2) (subactivity ?a2 ?a3)) (subactivity ?a1 ?a3))) ;;;; Axiom 5 The subactivity relation is a discrete ordering, so every ;; activity has an upwards successor in the ordering. ;;
(forall (?a1 ?a2) (=> (and (subactivity ?a1 ?a2) (not (equal ?a1 ?a2))) (exists (?a3) (and (subactivity ?a1 ?a3) (subactivity ?a3 ?a2) (not (equal ?a3 ?a1)) (forall (?a4) (=> (and (subactivity ?a1 ?a4) (subactivity ?a4 ?a3)) (or (equal ?a4 ?a1) (equal ?a4 ?a3)))))))) ;;;; Axiom 6 The subactivity relation is a discrete ordering, so every ;; activity has a downwards successor in the ordering. ;;
(forall (?a1 ?a2) (=> (and (subactivity ?a1 ?a2) (not (equal ?a1 ?a2))) (exists (?a3) (and (subactivity ?a1 ?a3) (subactivity ?a3 ?a2) (not (equal ?a3 ?a1)) (forall (?a4) (=> (and (subactivity ?a3 ?a4) (subactivity ?a4 ?a2)) (or (equal ?a4 ?a2) (equal ?a4 ?a3)))))))) ;;;;
(forall (?a) (<=> (primitive ?a) (and (activity ?a) (forall (?a1) (=> (subactivity ?a1 ?a) (equal ?a1 ?a)))))) ;;;;
;; ;; ;;
;;;; The core theory subactivity.th alone does not specify any relationship ;; between the occurrence of an activity and occurrences of its subactivities. ;; For example, the specification of subactivities alone does not allow us to ;; distinguish between a nondeterministic activity and a deterministic activity. ;;
;; The basic ontological commitments of the Subactivity Theory are based on the ;; following intuitions: ;;
;; Intuition 1: ;;
;; ;; The composition relation is a discrete partial ordering, in which ;; primitive activities are the minimal elements. ;; ;;
;;
;; (subactivity ?a1 ?a2) is TRUE in an interpretation of Subactivity ;; Theory if and only if activity ?a1 is a subactivity of activity ?a2. ;;
;; (primitive ?a) is TRUE in an interpretation of Subactivity Theory ;; if and only if the activity ?a has no proper subactivities. ;;
;;
;;
;; Last Updated: Wednesday, 15-December-2003 11:42:40
;; Return to the PSL homepage ;;
;; ;; ;; ;;;; Extension Name: duration.th
;; Primitive Lexicon:
;; Predicates: ;;
;; Defined Lexicon:
;; Functions: ;;
;;
;;
(and (timeduration zero) (timeduration max+) (timeduration max-)) ;;;; Axiom 2 ;; ;; The result of adding two timedurations is a timeduration. ;; ;;
(forall (?d1 ?d2) (=> (and (timeduration ?d1) (timeduration ?d2)) (timeduration (add ?d1 ?d2)))) ;;;; Axiom 3 ;; ;; The add function is associative. ;; ;;
(forall (?d1 ?d2 ?d3)
(=> (and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(equal (add (add ?d1 ?d2) ?d3) (add ?d1 (add ?d2 ?d3)))))
;;
;; Axiom 4
;;
;; zero is the additive identity.
;;
;;
(forall (?d)
(=> (timeduration ?d)
(equal (add ?d zero) ?d)))
;;
;; Axiom 5
;;
;; For any timeduration, there exists an additive inverse.
;;
;;
(forall (?d1)
(=> (timeduration ?d1)
(exists (?d2)
(and (timeduration ?d2)
(equal (add ?d1 ?d2) zero)))))
;;
;; Axiom 6
;;
;; The add function is commutative.
;;
;;
(forall (?d1 ?d2)
(=> (and (timeduration ?d1)
(timeduration ?d2))
(equal (add ?d1 ?d2) (add ?d2 ?d1))))
;;
;; Axiom 7
;;
;; The result of multiplying a timeduration by a scalar value is
;; a timeduration.
;;
;; (forall (?d ?r) (=> (timeduration ?d) (timeduration (mult ?r ?d)))) ;;;; Axiom 8 ;; ;; Multiplication by scalars: ;; ;;
(forall (?d1 ?d2 ?r)
(equal (mult ?r (add ?d1 ?d2)) (add (mult ?r ?d1) (mult ?r ?d2))))
;;
;; Axiom 9
;;
(forall (?d ?r ?s)
(equal (mult (add ?r ?s) ?d) (add (mult ?r ?d) (mult ?s ?d))))
;;
;; Axiom 10
;;
(forall (?d ?r ?s)
(equal (mult (mult ?r ?s) ?d) (mult ?r (mult ?s ?d))))
;;
;; Axiom 11
;;
;; one is the multiplicative identity.
;;
;;
(forall (?d)
(equal ?d (mult one ?d)))
;;
;; Axiom 12
;; Ordering Axioms for timedurations.
;;
(forall (?d1 ?d2 ?d3)
(=> (and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(<=> (lesser ?d1 ?d2)
(lesser (add ?d1 ?d3) (add ?d2 ?d3)))))
;;
;; Axiom 13
;;
(forall (?d1 ?d2 ?d3)
(=> (and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(<=> (equal ?d1 ?d2)
(equal (add ?d1 ?d3) (add ?d2 ?d3)))))
;;
;; Axiom 14
;;
;; max- is lesser than any timeduration, and
;; max+ is greater than any timeduration.
;;
;; (forall (?d) (=> (timeduration ?d) (and (lesser ?d max+) (lesser max- ?d)))) ;;;; Axiom 15 ;; ;; The result of adding any duration other than max+ to max- is max-, ;; and vice versa, the "sum" of max- and max+ is zero. ;; ;;
(forall (?d) (=> (timeduration ?d) (and (=> (not (equal ?d max-)) (equal max+ (add ?d max+))) (=> (not (equal ?d max+)) (equal max- (add ?d max-))) (equal zero (add max+ max-))))) ;;;; Axiom 16 ;; ;; The duration function assigns a timeduration to every pair ;; of timepoints. ;; ;;
(forall (?t1 ?t2) (=> (and (timepoint ?t1) (timepoint ?t2)) (timeduration (duration ?t1 ?t2)))) ;;;; Axiom 17 ;; ;; Every timeduration is equal to the value of the duration ;; function for some pair of timepoints. ;; ;;
(forall (?d)
(=> (timeduration ?d)
(exists (?t1 ?t2)
(and (timepoint ?t1)
(timepoint ?t2)
(equal ?d (duration ?t1 ?t2))))))
;;
;; Axiom 18
;;
;; The value of the duration function is zero if and only if
;; the two timepoints are equal.
;;
;; (forall (?t1 ?t2) (=> (and (timepoint ?t1) (timepoint ?t2)) (<=> (equal zero (duration ?t1 ?t2)) (equal ?t1 ?t2)))) ;;;; Axiom 19 ;; ;; The value of the duration function between ?t1 and ?t2 is the additive ;; inverse of the value of the duration function between ?t2 and ?t1. ;; ;;
(forall (?t1 ?t2) (=> (and (timepoint ?t1) (timepoint ?t2)) (equal zero (add (duration ?t1 ?t2) (duration ?t2 ?t1))))) ;;;; Axiom 20 ;; ;; Given a point i other than inf- or inf+, the duration from i to any point is ;; unique. ;; ;;
(forall (?t1 ?t2 ?t3) (=> (and (timepoint ?t1) (timepoint ?t2) (timepoint ?t3) (not (equal ?t1 inf-)) (not (equal ?t2 inf+)) (equal (duration ?t1 ?t2) (duration ?t1 ?t3))) (equal ?t1 ?t2))) ;;;; Axiom 21 ;; ;; The duration from any point other than inf- to inf- is max- and from any point ;; other than inf+ to inf+ is max+. ;; ;;
(forall (?t) (and (=> (and (timepoint ?t) (not (equal ?t inf-))) (equal max+ (duration inf- ?t))) (=> (and (timepoint ?t) (not (equal ?t inf+))) (equal max- (duration inf+ ?t))))) ;;;; Axiom 22 ;; ;; The duration from inf- to any point other than inf- is max+ and from inf+ to any ;; point other than inf+ is max-. ;; ;;
(forall (?t) (and (=> (and (timepoint ?t) (not (equal ?t inf-))) (equal max- (duration ?t inf-))) (=> (and (timepoint ?t) (not (equal ?t inf+))) (equal max+ (duration ?t inf+))))) ;;;;
(forall (?t1 ?t2 ?d) (<=> (equal ?t2 (time_add ?t1 ?d)) (and (timepoint ?t1) (timepoint ?t2) (timeduration ?d) (equal ?d (duration ?t2 ?t1))))) ;;;; ;; ;; ;;
;; Extension Name: envelope.th
;; Primitive Lexicon:
;; Relations: ;;
;; 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 ;;
;;
;;
(forall (?a1 ?s) (=> (root ?s ?a1) (exists (?a2) (envelope ?a2 ?a1 ?s)))) ;;;; Axiom 2 ;; ;; Every activity tree has an umbra activity. ;; ;;
(forall (?a1 ?s) (=> (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) (=> (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) (=> (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) (=> (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) (=> (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) (=> (and (envelope ?a2 ?a1 ?s) (occurrence_of ?o ?a2) (equal ?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) (=> (and (umbra ?a2 ?a1 ?s) (occurrence_of ?o ?a2) (equal ?s (root_occ ?o))) (unrestricted ?o))) ;;;; ;; ;;
;; Extension Name: preserve.th
;; Primitive Lexicon:
;; Relations: ;;
;; Relations: ;;
;; Definitional Extensions Required by this Extension: occ_precond.def ;;
;;
;;
(forall (?a1 ?a2 ?s1 ?s2) (=> (and (ubiquitous ?a1 ?a2) (min_precedes ?s1 ?s2 ?a2)) (exists (?s3 ?s4 ?s5 ?s6) (and (tree_equiv ?s1 ?s2) (tree_equiv ?s3 ?s4) (occurrence_of ?s5 ?a1) (occurrence_of ?s6 ?a1) (legal_equiv ?s5 ?s6) (end_iso ?s3 ?s4 ?s5 ?s6))))) ;;;; Axiom 2 ;; ;; ;;
(forall (?a1 ?a2 ?s1 ?s2) (=> (and (ubiquitous ?a1 ?a2) (min_precedes ?s1 ?s2 ?a2)) (not (exists (?s3 ?s4) (and (occurrence_of ?s3 ?a1) (occurrence_of ?s4 ?a1) (legal_equiv ?s3 ?s4) (end_iso ?s1 ?s2 ?s3 ?s4)))))) ;;;; Axiom 3 ;; ;; ;;
(forall (?a1 ?a2 ?s1 ?s2 ?s3 ?s4) (=> (and (ubiquitous ?a1 ?a2) (occurrence_of ?s3 ?a1) (occurrence_of ?s4 ?a1) (legal_equiv ?s3 ?s4) (end_iso ?s1 ?s2 ?s3 ?s4)) (exists (?o1 ?o2) (and (occurrence_of ?o1 ?a1) (occurrence_of ?o2 ?a1) (subactivity_occurrence ?s1 ?o1) (subactivity_occurrence ?s2 ?o1))))) ;;;;
(forall (?s1 ?s2 ?s3 ?s4) (<=> (end_iso ?s1 ?s2 ?s3 ?s4) (exists (?s5 ?s6) (and (precedes ?s5 ?s1) (precedes ?s5 ?s3) (precedes ?s6 ?s2) (precedes ?s6 ?s4) (tree_equiv ?s1 ?s2) (tree_equiv ?s3 ?s4) (tree_equiv ?s5 ?s6))))) ;;;; ;; ;;
;; Extension Name: soo.th
;; Primitive Lexicon:
;; Relations: ;;
;; Relations: ;;
;; Definitional Extensions Required by this Extension: none ;;
;;
;;
(forall (?s1 ?s2 ?a) (=> (soo_precedes ?s1 ?s2 ?a) (and (soo ?s1 ?a) (soo ?s2 ?a)))) ;;;; Axiom 2 ;; ;; Elements of the subactivity occurrence ordering are elements ;; of the activity tree. ;; ;;
(forall (?a ?s) (=> (soo ?s ?a) (or (root ?s ?a) (exists (?s1) (min_precedes ?s1 ?s ?a))))) ;;;; Axiom 3 ;; ;; The function soomap maps the activity tree to the subactivity occurrence ordering. ;; ;;
(forall (?s ?occ ?a)
(=> (and (occurrence_of ?occ ?a)
(subactivity_occurrence ?s ?occ)
(arboreal ?s))
(soo (soomap ?s) ?a)))
;;
;; Axiom 4
;;
;; The elements of the subactivity occurrence ordering are fixed by soomap.
;;
;; (forall (?s ?a) (=> (soo ?s ?a) (equal ?s (soomap ?s)))) ;;;; Axiom 5 ;; ;; The function soomap is a branch monomorphism. ;; ;;
(forall (?s ?a) (or (mono ?s (soomap ?s) ?a) (equal ?s (soomap ?s)))) ;;;; Axiom 6 ;; ;; The activity tree is order-homomorphic to the subactivity ;; occurrence ordering. ;; ;;
(forall (?a ?s1 ?s2) (=> (min_precedes ?s1 ?s2 ?a) (<=> (soo_precedes (soomap ?s1) (soomap ?s2) ?a) (not (exists (?s3 ?s4) (and (min_precedes ?s4 ?s3 ?a) (equal (soomap ?s3) (soomap ?s1)) (equal (soomap ?s4) (soomap ?s2)))))))) ;;;; Axiom 7 ;; soo_precedes is not symmetric. ;;
(forall (?a ?s1 ?s2) (=> (soo_precedes ?s1 ?s2 ?a) (not (soo_precedes ?s2 ?s1 ?a)))) ;;;; Axiom 8 ;; soo_precedes is transitive. ;;
(forall (?a ?s1 ?s2 ?s3) (=> (and (soo_precedes ?s1 ?s2 ?a) (soo_precedes ?s2 ?s3 ?a)) (soo_precedes ?s1 ?s3 ?a))) ;;;;
(forall (?s ?a) (<=> (root_soo ?s ?a) (and (soo ?s ?a) (not (exists (?s1) (soo_precedes ?s1 ?s ?a)))))) ;;;; Definition 2 ;; An activity occurrence is a leaf of a subactivity occurrence ordering for an activity ?a ;; if and only if it is an element of the ordering and there does not exist an activity ;; occurrence that follows it in the ordering. ;;
(forall (?s ?a) (<=> (leaf_soo ?s ?a) (and (soo ?s ?a) (not (exists (?s1) (soo_precedes ?s ?s1 ?a)))))) ;;;; Definition 3 ;; An activity occurrence ?s2 is the next subactivity occurrence after ?s1 ;; in a subactivity occurrence ordering for ?a if and only of ?s1 precedes ?s2 ;; in the ordering and there does not exist a subactivity occurrence that is between ;; them in the ordering. ;;
(forall (?s1 ?s2 ?a) (<=> (next_subactivity ?s1 ?s2 ?a)
(and (soo_precedes ?s1 ?s2 ?a)
(not (exists (?s3)
(and (soo_precedes ?s1 ?s3 ?a)
(soo_precedes ?s3 ?s2 ?a)))))))
;;
;;
;;
;; ;; Extension Name: requires.th
;; Primitive Lexicon:
;; Relations: ;;
;; Definitional Extensions Required by this Extension: None
;;
;;
;;
(forall (?a ?a1 ?r ?s) (=> (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)
(<=> (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)
(<=> (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) (=> (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)
(<=> (prior (demand (conc ?a1 ?a2) ?r ?q) ?s)
(exists (?q1 ?q2)
(and (prior (demand ?a1 ?r ?q1) ?s)
(prior (demand ?a2 ?r ?q2) ?s)
(equal ?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) (<=> (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) (equal ?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) (equal ?q1 (plus ?q ?q2))))))) ;;;;
;; ;;
;;;; Extension Name: res_set.th
;; Primitive Lexicon: ;;
;; Definitional Extensions Required by this Extension: None ;;
;;
;;
(forall (?i ?r ?occ)
(=> (holds (resource_set ?i ?r) ?occ)
(forall (?rp)
(=> (set_member ?rp ?i)
(exists (?a)
(requires ?a ?rp))))))
;;
;;
(forall (?i ?r1 ?r2 ?a ?occ)
(=> (and (holds (resource_set ?i ?r1) ?occ)
(set_member ?r2 ?i)
(requires ?a ?r2))
(requires ?a ?r1)))
;;
;;
(forall (?i1 ?i2 ?r ?occ)
(=> (and (holds (resource_set ?i1 ?r) ?occ)
(holds (resource_set ?i2 ?r) ?occ))
(equal ?i1 ?i2)))
;;
;;
(forall (?r1 ?r2 ?occ)
(<=> (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)
(<=> (holds (resource_subset ?r1 ?r2) ?occ)
(forall (?r ?i1 ?i2)
(=> (and (holds (resource_set ?i1 ?r1) ?occ)
(holds (resource_set ?i2 ?r2) ?occ)
(set_member ?r ?i1))
(set_member ?r ?i2)))))
;;