Occurrence Trees

Occurrence Trees

Extension Name: occtree.th

Primitive Lexicon:

Relations:

Functions: Defined Lexicon:

Relations:

Theories Required by this Extension: psl_core.th

Definitional Extensions Required by this Extension: None

Axioms

Axiom 1 The earlier relation is restricted to arboreal activity occurrences (that is, activity occurrences that are elements of the occurrence tree). 
(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(and	(arboreal ?s1)
			(arboreal ?s2))))
Axiom 2 The ordering relation over occurrences is irreflexive. 
(forall (?s1 ?s2)
	(if	(earlier ?s1 ?s2)
		(not (earlier ?s2 ?s1))))
Axiom 3 The ordering relation over occurrences is transitive. 
(forall (?s1 ?s2 ?s3)
	(if	(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)
	(if	(and	(earlier ?s1 ?s2)
			(earlier ?s3 ?s2))
		(or	(earlier ?s1 ?s3)
			(earlier ?s3 ?s1)
			(= ?s3 ?s1))))
Axiom 5 No occurrence in the occurrence tree is earlier than an initial occurrence. 
(forall (?s)
	(iff	(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)
	(if	(earlier ?s1 ?s2)
		(exists (?sp)
			(and	(initial ?sp)
				(earlierEq ?sp ?s1)))))
Axiom 7 There is an initial occurrence of each activity. 
(forall (?s ?a)
        (if	(occurrence_of ?s ?a)
		(iff	(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)
	(if	(and	(initial ?s1)
			(initial ?s2)
			(occurrence_of ?s1 ?a)
			(occurrence_of ?s2 ?a))
		(= ?s1 ?s2)))
Axiom 9 The successor of an arboreal activity occurrence is an occurrence of a generator activity. 
(forall (?a ?o)
        (iff    (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)
        (if	(earlier ?s1 ?s2)
		(exists (?a ?s3)
                        (and    (generator ?a)
                                (= ?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)
        (if	(generator ?a)
		(iff	(earlier ?s1 (successor ?a ?s2))
			(earlierEq ?s1 ?s2))))
Axiom 12 The legal relation restricts arboreal activity occurrences. 
(forall (?s)
	(if	(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)
	(if	(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)
	(if	(earlier ?s1 ?s2)
		(before (endof ?s1) (beginof ?s2))))

Definitions

Definition 1 An activity occurrence ?s1 precedes another activity occurrence ?s2 if and only if ?s1 is earlier than ?s2 in the occurrence tree and ?s2 is legal. 
(forall (?s1 ?s2) (iff (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) (iff (earlierEq ?s1 ?s2)
(and	(arboreal ?s1)
	(arboreal ?s2)
	(or	(earlier ?s1 ?s2)
		(= ?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) (iff (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) (iff  (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) (iff  (arboreal ?s)
(exists (?sp)
        (earlier ?s ?sp))))
  ;;