Definition 1. Timepoint q is between timepoints p and r iff p is before q and q is before r.
(defrelation Between (?p ?q ?r) := (and (Before ?p ?q) (Before ?q ?r)))
Definition 2. Timepoint p is BeforeEq timepoint q iff p is before or equal to q.
(defrelation BeforeEq (?p ?q) :=
(and (Point ?p) (Point ?q)
(or (Before ?p ?q) (= ?p ?q))))Definition 3. Timepoint q is BetweenEq timepoints p and r iff p is before or equal to q, and q is before or equal to r.
(defrelation BetweenEq (?p ?q ?r) :=
(and (BeforeEq ?p ?q)
(BeforeEq ?q ?r)))
Definition 4. An object exists-at a timepoint p iff p is BetweenEq its begin and end points.
(defrelation Exists-at (?x ?p) :=
(and (Object ?x)
(BetweenEq (Beginof ?x) ?p (Endof ?x))))
Definition 5. An activity is-occurring-at a timepoint p iff p is BetweenEq the activity's begin and end points.
(defrelation Is-occurring-at (?a ?p) :=
(and (Activity ?a)
(BetweenEq (Beginof ?a) ?p (Endof ?a))))
Definition 6. a is a subactivity of b iff every object in a at a timepoint t is also in b at t, and b is occuring at every timepoint that a is.
(defrelation Subactivity (?a ?b) :=
(and (forall (?x ?t)
(=> (In ?x ?a ?t)
(In ?x ?b ?t))
(forall ?p
(=> (Is-occurring-at ?a ?p)
(Is-occurring-at ?b ?p)))))
Definition 7. Activity a immediately precedes activity b iff a's endpoint is b's beginpoint.
(defrelation Imm-precedes (?a ?b) :=
(and (Activity ?a)
(Activity ?b)
(= (Endof ?a) (Beginof ?b))))
Axiom 1. The Before relation only holds between timepoints.
(=> (Before ?p ?q)
(and (Point ?p) (Point ?q)))
Axiom 2. The Before relation is a total ordering.
(=> (and (Point ?p) (Point ?q))
(or (= ?p ?q) (Before ?p ?q) (Before ?q ?p)))
Axiom 3. The Before relation is irreflexive.
(not (Before ?p ?p))
Axiom 4. The Before relation is transitive.
(=> (and (Before ?p ?q) (Before ?q ?r)
(Before ?p ?r))
Axiom 5: The timepoint inf- is before all other timepoints.
(=> (and (Point ?t) (not (= ?t inf-)))
(Before inf- ?t))
Axiom 6. Every other timepoint is before inf+.
(=> (and (Point ?t) (not (= ?t inf+)))
(Before ?t inf+))
Axiom 7. Given any timepoint t other than inf-, there is a timepoint between inf- and t.
(=> (and (Point ?t) (not (= ?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+.
(=> (and (Point ?t) (not (= ?t inf+)))
(exists ?u (Between ?t ?u inf+)))
Axiom 9. Everything is either an activity, object, or timepoint.
(or (Activity ?x) (Object ?x) (Point ?x))
Axiom 10. Objects, activities, and timepoints are all distinct kinds of things.
(and (=> (Activity ?x)
(not (or (Object ?x) (Point ?x))))
(=> (Object ?x)
(not (Point ?x))))
Axiom 11. The begin and end of an activity are timepoints.
(=> (Activity ?a)
(and (Point (Beginof ?a))
(Point (Endof ?a))))
Axiom 12. The begin point of every activity is before or equal to its end point.
(=> (or (Activity ?x) (Object ?x))
(BeforeEq (Beginof ?x) (Endof ?x)))
Axiom 13. The participates-in relation only holds between objects, activities, and timepoints, respectively.
(=> (In ?x ?a ?t)
(and (Object ?x) (Activity ?a) (Point ?t)))
Axiom 14. An object can participate in an activity only at those timepoints at which both the object exists and the activity is occurring.
(=> (In ?x ?a ?t)
(and (Exists-at ?x ?t)
(Is-occurring-at ?a ?t)))
Axiom 15. Activities that are subactivities of each other (and hence which contain the same objects at the same timepoints and which are occurring at the same timepoints) are identical.
(=> (and (subactivity ?a ?b)
(subactivity ?b ?a))
(= ?a1 ?a2))