Theory of Complex Activities

Extension Name: complex.th

Primitive Lexicon:

(min_precedes ?s1 ?s2 ?a)
(root ?s ?a)

Defined Lexicon:

(do ?a ?s1 ?s2)
(leaf ?s ?a)
(next_subocc ?s1 ?s2 ?a)
(subtree ?s ?a1 ?a2)
(sibling ?s1 ?s2 ?a)

Theories Required by this Extension: occtree.th, atomic.th, subactivity.th, psl_core.th

Definitional Extensions Required by this Extension: None

Axioms

Axiom 1 Occurrences in the activity tree for an activity correspond to atomic subactivity occurrences of the activity.

(forall (?a ?s1 ?s2)
	(if	(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)
	(if	(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)
	(if	(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)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?s3)
			(and	(root ?s3 ?a)
				(or	(min_precedes ?s3 ?s1 ?a)
					(= ?s3 ?s1))))))

Axiom 5 No subactivity occurrences in an activity tree occur earlier than the root subactivity occurrence.

(forall (?s ?a)
	(if	(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)
	(if	(min_precedes ?s1 ?s2 ?a)
		(precedes ?s1 ?s2)))

Axiom 7 Root occurrences are elements of the occurrence tree.

(forall (?s ?a)
	(if	(root ?s ?a)
		(legal ?s)))

Axiom 8 Every legal atomic activity occurrence is an activity tree containing only one occurrence.

(forall (?a1 ?a2 ?s)
        (if	(and    (atomic ?a1)
                        (occurrence_of ?s ?a1)
                        (legal ?s)
			(subactivity ?a2 ?a1))
		(root ?s ?a2)))

Axiom 9 Activity trees are discrete.

(forall (?s1 ?s2 ?a)
	(if	(min_precedes ?s1 ?s2 ?a)
		(exists (?s3)
			(and	(next_subocc ?s1 ?s3 ?a)
				(or	(min_precedes ?s3 ?s2 ?a)
					(= ?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)
	(if	(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)
	(if	(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)
        (if	(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)
	(if	(and	(min_precedes ?s2 ?s1 ?a)
			(min_precedes ?s3 ?s1 ?a)
			(precedes ?s2 ?s3))
		(min_precedes ?s2 ?s3 ?a)))

Definitions

Definition 1 An occurrence is the leaf of an activity tree if and only if there exists an earlier atomic subactivity occurrence but there does not exist a later atomic subactivity occurrence.

(forall (?s ?a) (iff (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) (iff (do ?a ?s1 ?s2)
(and	(root ?s1 ?a)
	(leaf ?s2 ?a)
	(or	(min_precedes ?s1 ?s2 ?a)
		(= ?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) (iff (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) (iff (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) (iff (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	(= ?s1 (successor ?a1 ?s4))
					(= ?s2 (successor ?a2 ?s4)))))))))