;; lisp2explicit: Thu Sep 5 16:26:59 EDT 2002 (defaxiom "2.1-1" (forall (t) (=> (instant t) (temporal-entity t)))) (defaxiom "2.1-2" (forall (T) (=> (interval T) (temporal-entity T)))) (defaxiom "2.1-3" (forall (T) (=> (temporal-entity T) (instant (beginning-of T))))) (defaxiom "2.1-4" (forall (T) (=> (temporal-entity T) (instant (end-of T))))) (defaxiom "2.1-5" (forall (t) (=> (instant t) (equals (beginning-of t) t)))) (defaxiom "2.1-6" (forall (t) (=> (instant t) (equals (end-of t) t)))) (defaxiom "2.1-7" (forall (t T) (=> (inside t T) (and (instant t) (interval T))))) (defaxiom "2.1-8" (forall (t T) (<=> (begins-or-in t T) (or (equals (beginning-of T) t) (inside t T))))) (defaxiom "2.1-9" (forall (T t1 t2) (=> (time-between T t1 t2) (and (and (temporal-entity T) (instant t1)) (instant t2))))) (defaxiom "2.1-10" (forall (T t1 t2) (<=> (time-between T t1 t2) (and (equals (beginning-of T) t1) (equals (end-of T) t2))))) (defaxiom "2.1-11" (forall (t) (<=> (proper-interval t) (and (interval t) (not-equals (beginning-of t) (end-of t)))))) (defaxiom "2.2-1" (forall (T1 T2) (<=> (before T1 T2) (before (end-of T1) (beginning-of T2))))) (defaxiom "2.2-2" (forall (T1 T2) (=> (before T1 T2) (not-equals T1 T2)))) (defaxiom "2.2-3" (forall (T1 T2) (=> (before T1 T2) (not (before T2 T1))))) (defaxiom "2.2-4" (forall (T1 T2 T3) (=> (and (before T1 T2) (before T2 T3)) (before T1 T3)))) (defaxiom "2.2-5" (forall (t) (=> (not-equals t *NegInf*) (before *NegInf* t)))) (defaxiom "2.2-6" (forall (t) (=> (not-equals t *PosInf*) (before t *PosInf*)))) (defaxiom "2.2-7" (forall (T) (=> (interval T) (not (before (end-of T) (beginning-of T)))))) (defaxiom "2.2-8" (forall (T) (=> (proper-interval T) (before (beginning-of T) (end-of T))))) (defaxiom "2.2-9" (forall (t1 t2) (=> (and (and (instant t1) (instant t2)) (before t1 t2)) (exists (T) (time-between T t1 t2))))) (defaxiom "2.2-10" (forall (t T) (=> (inside t T) (and (before (beginning-of T) t) (before t (end-of T)))))) (defaxiom "2.2-11" (forall (T1 T2) (<=> (after T1 T2) (before T2 T1)))) (defaxiom "2.3-1" (forall (T1 T2) (=> (int-equals T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-2" (forall (T1 T2) (=> (int-before T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-3" (forall (T1 T2) (=> (int-meets T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-4" (forall (T1 T2) (=> (int-overlaps T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-5" (forall (T1 T2) (=> (int-starts T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-6" (forall (T1 T2) (=> (int-during T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-7" (forall (T1 T2) (=> (int-finishes T1 T2) (and (proper-interval T1) (proper-interval T2))))) (defaxiom "2.3-8" (forall (T1 T2) (<=> (int-equals T1 T2) (and (equals (beginning-of T1) (beginning-of T2)) (equals (end-of T1) (end-of T2)))))) (defaxiom "2.3-9" (forall (T1 T2) (<=> (int-before T1 T2) (before T1 T2)))) (defaxiom "2.3-10" (forall (T1 T2) (<=> (int-after T1 T2) (after T1 T2)))) (defaxiom "2.3-11" (forall (T1 T2) (<=> (int-meets T1 T2) (equals (end-of T1) (beginning-of T2))))) (defaxiom "2.3-12" (forall (T1 T2) (<=> (int-met-by T1 T2) (int-meets T2 T1)))) (defaxiom "2.3-13" (forall (T1 T2) (<=> (int-overlaps T1 T2) (and (and (before (beginning-of T1) (beginning-of T2)) (before (beginning-of T2) (end-of T1))) (before (end-of T1) (end-of T2)))))) (defaxiom "2.3-14" (forall (T1 T2) (<=> (int-overlapped-by T1 T2) (int-overlaps T2 T1)))) (defaxiom "2.3-15" (forall (T1 T2) (<=> (int-starts T1 T2) (and (equals (beginning-of T1) (beginning-of T2)) (before (end-of T1) (end-of T2)))))) (defaxiom "2.3-16" (forall (T1 T2) (<=> (int-started-by T1 T2) (int-starts T2 T1)))) (defaxiom "2.3-17" (forall (T1 T2) (<=> (int-during T1 T2) (and (before (beginning-of T2) (beginning-of T1)) (before (end-of T1) (end-of T2)))))) (defaxiom "2.3-18" (forall (T1 T2) (<=> (int-contains T1 T2) (int-during T2 T1)))) (defaxiom "2.3-19" (forall (T1 T2) (<=> (int-finishes T1 T2) (and (before (beginning-of T2) (beginning-of T1)) (equals (end-of T1) (end-of T2)))))) (defaxiom "2.3-20" (forall (T1 T2) (<=> (int-finished-by T1 T2) (int-finishes T2 T1)))) (defaxiom "2.3-21" (forall (T1 T2) (<=> (starts-or-during T1 T2) (or (int-starts T1 T2) (int-during T1 T2))))) (defaxiom "2.3-22" (forall (T1 T2) (<=> (nonoverlap T1 T2) (or (or (or (int-before T1 T2) (int-after T1 T2)) (int-meets T1 T2)) (int-met-by T1 T2))))) (defaxiom "2.4-1" (forall (t1 t2) (=> (and (instant t1) (instant t2)) (or (or (before t1 t2) (equals t1 t2)) (before t1 t2))))) (defaxiom "2.4-2" (forall (t) (=> (instant t) (or (before t *PosInf*) (equals t *PosInf*))))) (defaxiom "2.4-3" (forall (t1) (=> (instant t1) (exists (t2) (and (and (instant t2) (before t1 t2)) (before t2 *PosInf*)))))) (defaxiom "2.4-4" (forall (t) (=> (instant t) (or (equals t *NegInf*) (before *NegInf* t))))) (defaxiom "2.4-5" (forall (t1) (=> (instant t1) (exists (t2) (and (and (instant t2) (before t2 t1)) (before *NegInf* t2)))))) (defaxiom "2.4-6" (forall (t1) (=> (instant t1) (exists (t2) (and (instant t2) (before t1 t2)))))) (defaxiom "2.4-7" (forall (t1) (=> (instant t1) (exists (t2) (and (instant t2) (before t2 t1)))))) (defaxiom "2.4-8" (forall (t1 t2) (=> (and (and (instant t1) (instant t2)) (before t1 t2)) (exists (t) (and (and (instant t) (before t1 t)) (before t t2)))))) (defaxiom "2.4-9" (forall (T t) (=> (and (before (beginning-of T) t) (before t (end-of T))) (inside t T)))) (defaxiom "2.4-10" (forall (T1 T2) (=> (int-equals T1 T2) (equals T1 T2)))) (defaxiom "2.5-1" (forall (e t) (=> (at-time e t) (instant t)))) (defaxiom "2.5-2" (forall (e T) (=> (during e T) (interval T)))) (defaxiom "2.5-3" (forall (e T t) (=> (and (during e T) (inside t T)) (at-time e t)))) (defaxiom "2.5-4" (forall (T e) (=> (time-span-of T e) (temporal-entity T)))) (defaxiom "2.5-5" (forall (T e) (=> (and (time-span-of T e) (interval T)) (during e T)))) (defaxiom "2.5-6" (forall (t e) (=> (and (time-span-of t e) (instant t)) (at-time e t)))) (defaxiom "2.5-7" (forall (T e t1) (=> (and (and (and (and (time-span-of T e) (interval T)) (not (inside t1 T))) (not (beginning-of t1 T))) (not (end-of t1 T))) (not (at-time e t1))))) (defaxiom "2.5-8" (forall (t e t1) (=> (and (and (time-span-of t e) (instant t)) (not-equals t1 t)) (not (at-time e t1))))) (defaxiom "3.1-1" (forall (T) (equals (seconds T) (duration T *Second*)))) (defaxiom "3.1-2" (forall (T) (equals (minutes T) (duration T *Minute*)))) (defaxiom "3.1-3" (forall (T) (equals (hours T) (duration T *Hour*)))) (defaxiom "3.1-4" (forall (T) (equals (days T) (duration T *Day*)))) (defaxiom "3.1-5" (forall (T) (equals (weeks T) (duration T *Week*)))) (defaxiom "3.1-6" (forall (T) (equals (months T) (duration T *Month*)))) (defaxiom "3.1-7" (forall (T) (equals (years T) (duration T *Year*)))) (defaxiom "3.1-8" (forall (T u) (=> (duration T u) (and (proper-interval T) (temporal-unit u))))) (defaxiom "3.1-9" (forall (T) (equals (seconds T) (times 60 (minutes T))))) (defaxiom "3.1-10" (forall (T) (equals (minutes T) (times 60 (hours T))))) (defaxiom "3.1-11" (forall (T) (equals (hours T) (times 24 (days T))))) (defaxiom "3.1-12" (forall (T) (equals (days T) (times 7 (weeks T))))) (defaxiom "3.1-13" (forall (T) (equals (months T) (times 12 (years T))))) (defaxiom "3.2-1" (forall (x S) (<=> (concatenation x S) (and (and (and (and (proper-interval x) (forall (z) (=> (begins-or-in z x) (exists (y) (and (member y S) (begins-or-in z y)))))) (forall (z) (=> (equals (end-of x) z) (exists (y) (and (member y S) (equals (end-of y) z)))))) (forall (y) (=> (member y S) (or (or (int-starts y x) (int-during y x)) (int-finishes y x))))) (forall (y1 y2) (=> (and (member y1 S) (member y2 S)) (or (equals y1 y2) (nonoverlap y1 y2)))))))) (defaxiom "3.2-2" (forall (N u x) (<=> (Hath N u x) (exists (S) (and (and (equals (card S) N) (forall (z) (=> (member z S) (equals (duration z u) 1)))) (concatenation x S)))))) (defaxiom "3.2-3" (forall (N u x) (=> (Hath N u x) (and (and (integer N) (temporal-unit u)) (proper-interval x))))) (defaxiom "3.3-1" (forall (T) (<=> (second T) (equals (seconds T) 1)))) (defaxiom "3.3-2" (forall (T) (<=> (minute T) (equals (minutes T) 1)))) (defaxiom "3.3-3" (forall (T) (<=> (hour T) (equals (hours T) 1)))) (defaxiom "3.3-4" (forall (T) (<=> (day T) (equals (days T) 1)))) (defaxiom "3.3-5" (forall (T) (<=> (week T) (equals (weeks T) 1)))) (defaxiom "3.3-6" (forall (T) (<=> (month T) (equals (months T) 1)))) (defaxiom "3.3-7" (forall (T) (<=> (year T) (equals (years T) 1)))) (defaxiom "3.3-8" (forall (T) (=> (minute T) (Hath 60 *Second* T)))) (defaxiom "3.3-9" (forall (T) (=> (hour T) (Hath 60 *Minute* T)))) (defaxiom "3.3-10" (forall (T) (=> (day T) (Hath 24 *Hour* T)))) (defaxiom "3.3-11" (forall (T) (=> (week T) (Hath 7 *Day* T)))) (defaxiom "3.3-12" (forall (T) (=> (year T) (Hath 12 *Month* T)))) (defaxiom "4.2-1" (forall (y n x) (<=> (<=> (sec y n x) (equals (secFn n x) y)) (clock-int y n *sec* x)))) (defaxiom "4.2-2" (forall (y n x) (<=> (<=> (minit y n x) (equals (minitFn n x) y)) (clock-int y n *min* x)))) (defaxiom "4.2-3" (forall (y n x) (<=> (<=> (hr y n x) (equals (hrFn n x) y)) (clock-int y n *hr* x)))) (defaxiom "4.2-4" (forall (y n x) (<=> (<=> (da y n x) (equals (daFn n x) y)) (cal-int y n *da* x)))) (defaxiom "4.2-5" (forall (y n x) (<=> (<=> (mon y n x) (equals (monFn n x) y)) (cal-int y n *mon* x)))) (defaxiom "4.2-6" (forall (y n x) (<=> (<=> (yr y n x) (equals (yrFn n x) y)) (cal-int y n *yr* x)))) (defaxiom "4.2-7" (forall (y n x) (<=> (hr12 y n *am* x) (hr y n x)))) (defaxiom "4.2-8" (forall (y n x) (<=> (hr12 y n *pm* x) (hr y (plus n 12) x)))) (defaxiom "4.2-9" (forall (y n x) (=> (sec y n x) (second y)))) (defaxiom "4.2-10" (forall (y n x) (=> (minit y n x) (minute y)))) (defaxiom "4.2-11" (forall (y n x) (=> (hr y n x) (hour y)))) (defaxiom "4.2-12" (forall (y n x) (=> (da y n x) (day y)))) (defaxiom "4.2-13" (forall (y n x) (=> (mon y n x) (month y)))) (defaxiom "4.2-14" (forall (y n x) (=> (yr y n x) (year y)))) (defaxiom "4.2-15" (forall (y n u x n-1) (<=> (cal-int y n u x) (clock-int y n-1 u x)))) (defaxiom "4.2-16" (forall (y n u x) (=> (cal-int y n u x) (and (and (and (interval y) (integer n)) (temporal-unit u)) (interval x))))) (defaxiom "4.2-17" (and (and (and (and (and (temporal-unit *sec*) (temporal-unit *min*)) (temporal-unit *hr*)) (temporal-unit *da*)) (temporal-unit *mon*)) (temporal-unit *yr*))) (defaxiom "4.2-18" (and (temporal-unit *dayofweek*) (temporal-unit *wk*))) (defaxiom "4.2-19" (forall (y n u x N) (=> (and (cal-int y n u x) (Hath N u x)) (and (less-than 0 n) (less-than-or-equals n N))))) (defaxiom "4.2-20" (forall (N u x) (=> (Hath N u x) (exists! (y) (cal-int y 1 u x))))) (defaxiom "4.2-21" (forall (S N u x y) (=> (and (Hath S N u x) (cal-int y 1 u x)) (int-starts y x)))) (defaxiom "4.2-22" (forall (N u x) (=> (Hath N u x) (exists! (y) (cal-int y N u x))))) (defaxiom "4.2-23" (forall (N u x y) (=> (and (Hath N u x) (cal-int y N u x)) (int-finishes y x)))) (defaxiom "4.2-24" (forall (y1 n u x N) (=> (and (and (cal-int y1 n u x) (Hath N u x)) (less-than n N)) (exists! (y2) (and (cal-int y2 (plus n 1) u x) (int-meets y1 y2)))))) (defaxiom "4.2-25" (forall (y2 n u x N) (=> (and (and (cal-int y2 n u x) (Hath N u x)) (less-than 1 n)) (exists! (y1) (and (cal-int y1 (minus n 1) u x) (int-meets y1 y2)))))) (defaxiom "4.3-1" (forall (y n x) (<=> (<=> (wk y n x) (equals (wkFn n x) y)) (cal-int y n *wk* x)))) (defaxiom "4.3-2" (forall (y n x) (=> (wk y n x) (week y)))) (defaxiom "4.3-3" (forall (y n x) (<=> (<=> (dayofweek y n x) (equals (dayofweekFn n x) y)) (cal-int y n *dayofweek* x)))) (defaxiom "4.3-4" (forall (y n x) (=> (dayofweek y n x) (exists (n1 x1) (wk x n1 x1))))) (defaxiom "4.3-5" (forall (y x) (<=> (dayofweek y 1 x) (Sunday y x)))) (defaxiom "4.3-6" (forall (y x) (<=> (dayofweek y 2 x) (Monday y x)))) (defaxiom "4.3-7" (forall (y x) (<=> (dayofweek y 3 x) (Tuesday y x)))) (defaxiom "4.3-8" (forall (y x) (<=> (dayofweek y 4 x) (Wednesday y x)))) (defaxiom "4.3-9" (forall (y x) (<=> (dayofweek y 5 x) (Thursday y x)))) (defaxiom "4.3-10" (forall (y x) (<=> (dayofweek y 6 x) (Friday y x)))) (defaxiom "4.3-11" (forall (y x) (<=> (dayofweek y 7 x) (Saturday y x)))) (defaxiom "4.3-12" (forall (y) (<=> (exists (n x) (dayofweek y n x)) (exists (n1 x1) (da y n1 x1))))) (defaxiom "4.3-13" (forall (z) (exists (x) (Tuesday (dayFn 1 (monFn 1 (yrFn 2002 (CE z)))) x)))) (defaxiom "4.3-14" (forall (y x) (<=> (weekday y x) (or (or (or (or (Monday y x) (Tuesday y x)) (Wednesday y x)) (Thursday y x)) (Friday y x))))) (defaxiom "4.3-15" (forall (y x) (<=> (weekendday y x) (or (Saturday y x) (Sunday y x))))) (defaxiom "4.4-1" (forall (y x) (<=> (mon y 1 x) (January y x)))) (defaxiom "4.4-2" (forall (y x) (<=> (mon y 2 x) (February y x)))) (defaxiom "4.4-3" (forall (y x) (<=> (mon y 3 x) (March y x)))) (defaxiom "4.4-4" (forall (y x) (<=> (mon y 4 x) (April y x)))) (defaxiom "4.4-5" (forall (y x) (<=> (mon y 5 x) (May y x)))) (defaxiom "4.4-6" (forall (y x) (<=> (mon y 6 x) (June y x)))) (defaxiom "4.4-7" (forall (y x) (<=> (mon y 7 x) (July y x)))) (defaxiom "4.4-8" (forall (y x) (<=> (mon y 8 x) (August y x)))) (defaxiom "4.4-9" (forall (y x) (<=> (mon y 9 x) (September y x)))) (defaxiom "4.4-10" (forall (y x) (<=> (mon y 10 x) (October y x)))) (defaxiom "4.4-11" (forall (y x) (<=> (mon y 11 x) (November y x)))) (defaxiom "4.4-12" (forall (y x) (<=> (mon y 12 x) (December y x)))) (defaxiom "4.4-13" (forall (m y) (=> (January m y) (Hath 31 *Day* m)))) (defaxiom "4.4-14" (forall (m y) (=> (March m y) (Hath 31 *Day* m)))) (defaxiom "4.4-15" (forall (m y) (=> (April m y) (Hath 30 *Day* m)))) (defaxiom "4.4-16" (forall (m y) (=> (May m y) (Hath 31 *Day* m)))) (defaxiom "4.4-17" (forall (m y) (=> (June m y) (Hath 30 *Day* m)))) (defaxiom "4.4-18" (forall (m y) (=> (July m y) (Hath 31 *Day* m)))) (defaxiom "4.4-19" (forall (m y) (=> (August m y) (Hath 31 *Day* m)))) (defaxiom "4.4-20" (forall (m y) (=> (September m y) (Hath 30 *Day* m)))) (defaxiom "4.4-21" (forall (m y) (=> (October m y) (Hath 31 *Day* m)))) (defaxiom "4.4-22" (forall (m y) (=> (November m y) (Hath 30 *Day* m)))) (defaxiom "4.4-23" (forall (m y) (=> (December m y) (Hath 31 *Day* m)))) (defaxiom "4.4-24" (forall (y) (forall (z) (<=> (leap-year y) (exists (n x) (and (year y n (CE z)) (or (divides 400 n) (and (divides 4 n) (not (divides 100 n)))))))))) (defaxiom "4.4-25" (forall (m y) (=> (and (February m y) (leap-year y)) (Hath 29 *Day* m)))) (defaxiom "4.4-26" (forall (m y) (=> (and (February m y) (not (leap-year y))) (Hath 28 *Day* m)))) (defaxiom "4.4-27" (forall (T) (<=> (month T) (exists (d1 d2 n m1 m2 n1 y1 y2 n2 e) (and (and (and (and (and (and (begins-or-in (beginning-of T) d1) (begins-or-in (end-of T) d2)) (da d1 n m1)) (mon m1 n1 y1)) (yr y1 n2 e)) (da d2 n m2)) (or (mon m2 (plus n1 1) y1) (exists (y2) (and (and (equals n1 12) (mon m2 1 y2)) (yr y2 (plus n2 1) e))))))))) (defaxiom "4.5-1" (forall (t y m d h n s z) (<=> (time-of t y m d h n s z) (begins-or-in t (secFn s (minFn n (hrFn h (daFn d (monFn m (yrFn y (CE z))))))))))) (defaxiom "4.5-2" (forall (t y m d h n s z) (<=> (time-of t y m d h n s z) (exists (s1 n1 h1 d1 m1 y1 e) (and (and (and (and (and (and (and (begins-or-in t s1) (sec s1 s n1)) (min n1 n h1)) (hr h1 h d1)) (da d1 d m1)) (mon m1 m y1)) (yr y1 y e)) (CEPred e z))))))