# Time ontology in PDDL

From: Drew McDermott (drew.mcdermott@yale.edu)
Date: 10/21/02

• Next message: George Ferguson: "Re: Time ontology in PDDL"

```I have been translating George's KIF axiomitization of the temporal
ontology into PDDL.  This isn't much of a translation, seeing as how
they're both predicate calculus.  (Caveat: I changed a few things; see
below.)  Because PDDL allows explicitly declared domains, the
relationships among the various axioms should be a bit clearer.  Also,
PDDL is strict about predicate arity and other type issues, so the
fact that this formalization has made it through the type checker
gives me a bit more confidence that there are no "obvious" bugs.  See
the end of this message for the PDDL code.  I have not yet generated
the DAML-ized version, because I need my graduate students to tell me
how to run the tool that does it automatically!
In doing this translation, I ran into several not-so-obvious bugs in
the original axioms.  Or perhaps I'm misunderstanding.  Here are my
notes:

> In the second treatment of infinite time, what does (end-of T)
denote when T is a positive half-infinite interval?  (Similarly for
beginning-of and negative half-infinite intervals.)

> The axioms in daml-infinite-linear-time imply that
(before *PosInf* *PosInf*).

> Axioms 2.2-5 and 2.2-6 imply that *NegInf* is before all time
points, and *PosInf* after, even in branching time.  Is that what
was intended?

>
3.  An interval consists of the beginning and end nodes and all the
arcs between the beginning and end nodes but no intermediate
nodes.  So inside(t,T) is never true.  (This is a hard model
to motivate.)

Model 3 is Totally Ordered and has Extensional Collapse but not Convexity.

Surely model 3 satisfies convexity trivially.

The only way to avoid convexity is to have intervals with "holes."

> Why is duration defined only for proper intervals?  Shouldn't instants have
duration 0?

> Why the asterisks in *Second* et al?

> Axioms 4.2-1 et seq. assume <=> is associative and commutative, which it
isn't (unless this is a KIFism I'm unfamiliar with).

> Why do we need both *second* and *sec*?  (etc.)  What does
*DayOfWeek* denote exactly?  I realize that they are introduced in
connection with time intervals that lie on "official" boundaries,
such as next Friday, as opposed to some random 24-hour period.  I
just don't see how the extra temporal units contribute.  If we start
with an "era" (such as CE(..)), and carve intervals out by first
getting the n'th year, then the m'th day of that year, and so forth,
we can use the original units to keep track of how long each
interval is.  That's what happens in my version, which lacks all
temporal units except *second*, *minute*, *hour*, *day*, *week*,
*month*, and *year*.  I could make it look more like the original if
I understood the original.

> I disagree that we need both clock-int and cal-int.  Subintervals should
begin counting from 1 in all cases.  So what if 8:00 names the first
minute of the ninth hour of the day?

>
"Whereas it makes sense to talk about the nth day in a year or the nth
minute in a day or the nth day in a week, it does not really make
sense to talk about the nth day-of-the-week in anything other than a
week.  Thus we can restrict the x argument to be a calendar week."

What about the first Monday in October?

>
"Weeks are independent of months and years.  However, we can still talk
about the nth week in some larger period of time, e.g., the third week
of the month or the fifth week of the semester.  So the same three
modes of representation are appropriate for weeks as well."

What is the third week in a month that begins in the middle of a week?

-- Drew

****************************

Formalism begins here!

;;; Provisional trivial set theory
(define (domain set-theory)
(:requirements :numbers)
(:types Set)

(:predicates (member x - Object s - Set))

(:functions (card s - Set) - Integer))

(define (domain daml-time)
(:requirements :equality :fluents)
(:extends set-theory)

(:types Temporal-entity Eventuality - Object
Interval - Temporal-entity
Instant Proper-interval - Interval)

(:objects *NegInf* *PosInf* - Instant)

(:functions
(beginning-of te - Temporal-entity)
(end-of te - Temporal-entity)
- Instant)

(:predicates
(begins-or-in t1 - Instant t2 - Interval)
(inside t1 - Instant t2 - Interval)
(time-between tv - Interval ts1 ts2 - Instant)
(before t1 t2 - Temporal-entity)
(after t1 t2 - Temporal-entity)
(int-equals tp1 tp2 - Proper-interval)
(int-before tp1 tp2 - Proper-interval)
(int-after tp1 tp2 - Proper-interval)
(int-meets tp1 tp2 - Proper-interval)
(int-overlaps tp1 tp2 - Proper-interval)
(int-starts tp1 tp2 - Proper-interval)
(int-during tp1 tp2 - Proper-interval)
(int-finishes tp1 tp2 - Proper-interval)
(int-finished-by tp1 tp2 - Proper-interval)
(int-contains tp1 tp2 - Proper-interval)
(int-met-by tp1 tp2 - Proper-interval)
(int-overlapped-by tp1 tp2 - Proper-interval)
(int-started-by tp1 tp2 - Proper-interval)
(starts-or-during tv1 tv2 - Interval)
(nonoverlap tv1 tv2 - Interval)

(at-time e - Eventuality ti - Instant)
(during e - Eventuality int - Interval)
(time-span-of int - Temporal-entity e - Eventuality)

(concatenation int - Proper-interval s - Set)
)
)

(define (addendum 2.1-Instants-and-Intervals)
(:domain daml-time)
(:axioms
;; 2.1-5, 2.1-6
(forall (ti - Instant)
(and (= (beginning-of ti) ti)
(= (end-of ti) ti)))

;; 2.1-8
(forall (ts - Instant tv - Interval)
(iff (begins-or-in ts tv)
(or (= (beginning-of tv)
ts)
(inside ts tv))))

;; 2.1-10
(forall (tv - Interval ts1 ts2 - Instant)
(iff (time-between tv ts1 ts2)
(and (= (beginning-of tv) ts1)
(= (end-of tv) ts2))))

;; 2.1-11
(forall (tv - Proper-interval)
(not (= (beginning-of tv) (end-of tv))))

;; 2.1-11
(forall (tv - Interval)
(and (if (= (beginning-of tv)
(end-of tv))
(is Instant tv))
(if (not (= (beginning-of tv)
(end-of tv)))
(is Proper-interval tv))))
))

(define (addendum 2.2-before)
(:domain daml-time)

(:axioms

;; 2.2-1
(forall (t1 t2 - Temporal-entity)
(iff (before t1 t2)
(before (end-of t1) (beginning-of t2))))

;; 2.2-2
(forall (t1 t2 - Temporal-entity)
(if (before t1 t2) (not (= t1 t2))))

;; 2.2-3
(forall (t1 t2 - Temporal-entity)
(if (before t1 t2) (not (before t2 t1))))

;; 2.2-4
(forall (t1 t2 t3 - Temporal-entity)
(if (and (before t1 t2) (before t2 t3))
(before t1 t3)))

;; 2.2-5
(forall (ti - Instant)
(if (not (= ti *NegInf*)) (before *NegInf* ti)))

;; 2.2-6
(forall (ti - Instant)
(if (not (= ti *PosInf*)) (before ti *PosInf*)))

;; 2.2-7
(forall (ti - Interval)
(not (before (end-of ti)
(beginning-of ti))))

;; 2.2-7
(forall (tv - Interval)
(not (before (end-of tv) (beginning-of tv))))

;; 2.2-8
(forall (tv - Proper-interval)
(before (beginning-of tv) (end-of tv)))

;; 2.2-9
(forall (t1 t2 - Instant)
(if (before t1 t2)
(exists (tv - Interval) (time-between tv t1 t2))))

;; 2.2-10
(forall (ts - Instant tv - Interval)
(if (inside ts tv)
(and (before (beginning-of tv) ts)
(before ts (end-of tv)))))

;; 2.2-11
(forall (t1 t2 - Temporal-entity)
(iff (after t1 t2) (before t2 t1)))
))

(define (addendum 2.3-Interval-relations)
(:domain daml-time)
(:axioms

;; 2.3-8
(forall (t1 t2 - Proper-interval)
(iff (int-equals t1 t2)
(and (= (beginning-of t1) (beginning-of t2))
(= (end-of t1) (end-of t2)))))

;; 2.3-9
(forall (t1 t2 - Proper-interval)
(iff (int-before t1 t2) (before t1 t2)))

;; 2.3-10
(forall (t1 t2 - Proper-interval)
(iff (int-after t1 t2) (after t1 t2)))

;; 2.3-11
(forall (t1 t2 - Proper-interval)
(iff (int-meets t1 t2)
(= (end-of t1) (beginning-of t2))))

;; 2.3-12
(forall (t1 t2 - Proper-interval)
(iff (int-met-by t1 t2)
(int-meets t2 t1)))

;; 2.3-13
(forall (t1 t2 - Proper-interval)
(iff (int-overlaps t1 t2)
(and (before (beginning-of t1) (beginning-of t2))
(before (beginning-of t2) (end-of t1))
(before (end-of t1) (end-of t2)))))

;; 2.3-14
(forall (t1 t2 - Proper-interval)
(iff (int-overlapped-by t1 t2)
(int-overlaps t2 t1)))

;; 2.3-15
(forall (t1 t2 - Proper-interval)
(iff (int-starts t1 t2)
(and (= (beginning-of t1) (beginning-of t2))
(before (end-of t1) (end-of t2)))))

;; 2.3-16
(forall (t1 t2 - Proper-interval)
(iff (int-started-by t1 t2)
(int-starts t2 t1)))

;; 2.3-17
(forall (t1 t2 - Proper-interval)
(iff (int-during t1 t2)
(and (before (beginning-of t2) (beginning-of t1))
(before (end-of t1) (end-of t2)))))

;; 2.3-18
(forall (t1 t2 - Proper-interval)
(iff (int-contains t1 t2) (int-during t2 t1)))

;; 2.3-19
(forall (tv1 tv2 - Proper-interval)
(iff (int-finishes tv1 tv2)
(and (before (beginning-of tv2) (beginning-of tv1))
(= (end-of tv1) (end-of tv2)))))

;; 2.3-20
(forall (tv1 tv2 - Proper-interval)
(iff (int-finished-by tv1 tv2) (int-finishes tv2 tv1)))

;; 2.3-21
(forall (tv1 tv2 - Proper-interval)
(iff (starts-or-during tv1 tv2)
(or (int-starts tv1 tv2) (int-during tv1 tv2))))

;; 2.3-22
(forall (tv1 tv2 - Proper-interval)
(iff (nonoverlap tv1 tv2)
(or (int-before tv1 tv2)
(int-after tv1 tv2)
(int-meets tv1 tv2)
(int-met-by tv1 tv2))))
))

(define (domain daml-linear-time)
(:extends daml-time)
(:axioms

;; 2.4-1
(forall (t1 t2 - Instant)
(or (before t1 t2) (= t1 t2) (before t2 t1)))))

(define (domain daml-infinite-linear-time)
(:extends daml-linear-time)

(:axioms

;; 2.4-2
(forall (ti - Instant)
(or (before ti *PosInf*) (= ti *PosInf*)))

;; 2.4-3
(forall (t1 - Instant)
(exists (t2 - Instant)
(and (before t1 t2) (before t2 *PosInf*))))

;; 2.4-4
(forall (ti - Instant)
(or (= ti *NegInf*) (before *NegInf* ti)))

;; 2.4-5
(forall (t1 - Instant)
(exists (t2 - Instant)
(and (before t2 t1) (before *NegInf* t2))))))

(define (domain daml-infinite-time)
(:extends daml-time)

(:predicates
(positive-half-infinite int - Interval)
(negative-half-infinite int - Interval))

(:axioms

;; 2.4-6
(forall (t1 - Instant)
(exists (t2 - Instant)
(before t1 t2)))

;; 2.4-7
(forall (t1 - Instant)
(exists (t2 - Instant)
(before t2 t1)))

(forall (int - Interval)
(iff (positive-half-infinite int)
(forall (t1 - Instant)
(if (inside t1 int)
(exists (t2 - Instant)
(and (inside t2 int) (before t1 t2)))))))

(forall (int - Interval)
(iff (negative-half-infinite int)
(forall (t1 - Instant)
(if (inside t1 int)
(exists (t2 - Instant)
(and (inside t2 int) (before t2 t1)))))))))

(define (domain daml-dense-time)
(:extends daml-time)

(:axioms

;; 2.4-8
(forall (t1 t2 - Instant)
(if (before t1 t2)
(exists (ti - Instant)
(and (before t1 ti) (before ti t2)))))))

(define (domain daml-convex-time)
(:extends daml-time)

(:axioms

;; 2.4-9
(forall (int - Interval ti - Instant)
(if (and (before (beginning-of int) ti)
(before ti (end-of int)))
(inside ti int)))))

(define (domain daml-extensional-time)
(:extends daml-time)

(:axioms

;; 2.4-10
(forall (int1 int2 - Proper-interval)
(if (int-equals int1 int2)
(= int1 int2)))))

(define (addendum 2.5-event-time)
(:domain daml-time)

(:axioms

;; 2.5-3
(forall (e - Eventuality int - Interval ti - Instant)
(if (and (during e int)
(inside ti int))
(at-time e ti)))

;; 2.5-5
(forall (te - Interval e - Eventuality)
(if (and (time-span-of te e)
(is Proper-interval te))
(during e te)))

;; 2.5-6
(forall (te - Interval e - Eventuality)
(if (and (time-span-of te e)
(is Instant te))
(at-time e te)))

;; 2.5-7
(forall (int - Interval e - Eventuality t1 - Instant)
(if (and (time-span-of int e)
(not (inside t1 int))
(not (= t1 (beginning-of int)))
(not (= t1 (end-of int))))
(not (at-time e t1))))

;; 2.5-8
(forall (ti ti1 - Instant e - Eventuality)
(if (and (time-span-of ti e)
(not (= ti1 ti)))
(not (at-time e ti1))))))

(define (addendum concat)
(:domain daml-time)

(:axioms

;; 3.2-1
(forall (x - Proper-interval s - Set)
(iff (concatenation x s)
(and (forall (z - Instant)
(if (begins-or-in z x)
(exists (y - Proper-interval)
(and (member y s)
(begins-or-in z y)))))
(forall (z - Instant)
(if (= (end-of x) z)
(exists (y - Proper-interval)
(and (member y s)
(= (end-of y) z)))))

(forall (y - Proper-interval)
(if (member y s)
(or (int-starts y x)
(int-during y x)
(int-finishes y x))))
(forall (y1 y2 - Proper-interval)
(if (and (member y1 s) (member y2 s))
(or (= y1 y2) (nonoverlap y1 y2)))))))))

(define (domain daml-time-measure)
(:requirements :numbers)
(:extends daml-time)

(:types Temporal-unit - Object)

(:functions
(seconds int - Proper-interval)
(minutes int - Proper-interval)
(hours int - Proper-interval)
(days int - Proper-interval)
(weeks int - Proper-interval)
(months int - Proper-interval)
(years int - Proper-interval)
(duration int - Proper-interval tu - Temporal-unit)
- Number)

(:predicates
(hath n - Integer u - Temporal-unit x - Proper-interval)
(second int - Proper-interval)
(minute int - Proper-interval)
(hour int - Proper-interval)
(day int - Proper-interval)
(week int - Proper-interval)
(month int - Proper-interval)
(year int - Proper-interval))

(:objects *second* *minute* *hour* *day* *week* *month* *year*
- Temporal-unit)

(:axioms

;; 3.2-2
(forall (n - Integer u - Temporal-unit x - Proper-interval)
(iff (hath n u x)
(exists (s - Set)
(and (= (card s) n)
(forall (z - Proper-interval)
(if (member z s) (= (duration z u) 1)))
(concatenation x s)))))

;; 3.1-1, ..., 3.1-7
(forall (int - Proper-interval)
(and (= (seconds int) (duration int *second*))
(= (minutes int) (duration int *minute*))
(= (hours int) (duration int *hour*))
(= (days int) (duration int *day*))
(= (weeks int) (duration int *week*))
(= (months int) (duration int *month*))
(= (years int) (duration int *year*))))

;; 3.1-9, ..., 3.1-13
(forall (int - Proper-interval)
(and (= (seconds int) (* 60 (minutes int)))
(= (minutes int) (* 60 (hours int)))
(= (hours int) (* 24 (days int)))
(= (months int) (* 12 (years int)))))

;; 3.3-1, ..., 3.3-7
(forall (int - Proper-interval)
(and (iff (second int) (= (seconds int) 1))
(iff (minute int) (= (minutes int) 1))
(iff (hour int) (= (hours int) 1))
(iff (day int) (= (days int) 1))
(iff (week int) (= (weeks int) 1))
(iff (month int) (= (months int) 1))
(iff (year int) (= (years int) 1))))

;; 3.3-8,...3.3-12
(forall (int - Proper-interval)
(and (if (minute int) (hath 60 *second* int))
(if (hour int) (hath 60 *minute* int))
(if (day int) (hath 24 *hour* int))
(if (week int) (hath 7 *day* int))
(if (year int) (hath 12 *month* int))))))

(define (domain daml-clock-calendar)
(:extends daml-extensional-time daml-time-measure)

(:types AM/PM Time-standard - Object
Era - Proper-interval)

(:objects *am* *pm* - AM/PM)

(:predicates
(sec y - Proper-interval n - Integer x - Proper-interval)
(minit y - Proper-interval n - Integer x - Proper-interval)
(hr y - Proper-interval n - Integer x - Proper-interval)
(hr12 y - Proper-interval n - Integer ap - AM/PM x - Proper-interval)
(da y - Proper-interval n - Integer x - Proper-interval)
(dayofweek y - Proper-interval n - Integer x - Proper-interval)
(wk y - Proper-interval n - Integer x - Proper-interval)
(mon y - Proper-interval n - Integer x - Proper-interval)
(yr y - Proper-interval n - Integer x - Proper-interval)

(clock-int y - Proper-interval n - Integer u - Temporal-unit
x - Proper-interval)

(cal-int y - Proper-interval n - Integer u - Temporal-unit
x - Proper-interval)

(sunday y x - Proper-interval)
(monday y x - Proper-interval)
(tuesday y x - Proper-interval)
(wednesday y x - Proper-interval)
(thursday y x - Proper-interval)
(friday y x - Proper-interval)
(saturday y x - Proper-interval)
(january y x - Proper-interval)
(february y x - Proper-interval)
(march y x - Proper-interval)
(april y x - Proper-interval)
(may y x - Proper-interval)
(june y x - Proper-interval)
(july y x - Proper-interval)
(august y x - Proper-interval)
(september y x - Proper-interval)
(october y x - Proper-interval)
(november y x - Proper-interval)
(december y x - Proper-interval)

(weekday x y - Proper-interval)
(weekendday x y - Proper-interval)

(leap-year x - Proper-interval)

(time-of t - Interval y m d h n s - Integer z - Time-standard))

(:functions
(secFn n - Integer x - Proper-interval)
(minitFn n - Integer x - Proper-interval)
(hrFn n - Integer x - Proper-interval)
(daFn n - Integer x - Proper-interval)
(dayofweekFn n - Integer x - Proper-interval)
(wkFn n - Integer x - Proper-interval)
(monFn n - Integer x - Proper-interval)
(yrFn n - Integer x - Proper-interval)
;;;;(hr12Fn n - Integer x - Proper-interval)
(nth-subinterval n - Integer u - Temporal-unit x - Proper-interval)
- Proper-interval
(CE s - Time-standard) - Era)

(:axioms

;; 4.2-1
(forall (x y - Proper-interval n - Integer)
(and (iff (sec y n x)
(clock-int y n *second* x))
(iff (sec y n x)
(= (secFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (secFn n x)
(nth-subinterval n *second* x)))

;; 4.2.-2
(forall (x y - Proper-interval n - Integer)
(and (iff (minit y n x)
(clock-int y n *minute* x))
(iff (minit y n x)
(= (minitFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (minitFn n x)
(nth-subinterval n *minute* x)))

;; 4.2-3
(forall (x y - Proper-interval n - Integer)
(and (iff (hr y n x)
(clock-int y n *hour* x))
(iff (hr y n x)
(= (hrFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (hrFn n x)
(nth-subinterval n *hour* x)))

;; 4.2-4
(forall (x y - Proper-interval n - Integer)
(and (iff (da y n x)
(cal-int y n *day* x))
(iff (da y n x)
(= (daFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (daFn n x)
(nth-subinterval n *day* x)))

;; 4.2-5
(forall (x y - Proper-interval n - Integer)
(and (iff (mon y n x)
(cal-int y n *month* x))
(iff (mon y n x)
(= (monFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (monFn n x)
(nth-subinterval n *month* x)))

;; 4.2-6
(forall (x y - Proper-interval n - Integer)
(and (iff (yr y n x)
(clock-int y n *year* x))
(iff (yr y n x)
(= (yrFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (yrFn n x)
(nth-subinterval n *year* x)))

;; 4.2-7, 4.2-8
(forall (x y - Proper-interval n - Integer)
(and (iff (hr12 y n *am* x)
(hr y n x))
(iff (hr12 y n *pm* x)
(hr y (+ n 12) x))))

;; 4.2-9
(forall (x y - Proper-interval n - Integer)
(if (sec y n x) (second y)))

;; 4.2-10
(forall (x y - Proper-interval n - Integer)
(if (minit y n x) (minute y)))

;; 4.2-11
(forall (x y - Proper-interval n - Integer)
(if (hr y n x) (hour y)))

;; 4.2-12
(forall (x y - Proper-interval n - Integer)
(if (da y n x) (day y)))

;; 4.2-13
(forall (x y - Proper-interval n - Integer)
(if (mon y n x) (month y)))

;; 4.2-14
(forall (x y - Proper-interval n - Integer)
(if (yr y n x) (year y)))

;; 4.2-15
(forall (y x - Proper-interval n - Integer u - Temporal-unit)
(iff (cal-int y n u x) (clock-int y (- n 1) u x)))

;; 4.2-19
(forall (y x - Proper-interval u - Temporal-unit n N - Integer)
(if (and (cal-int y n u x) (hath N u x))
(and (< 0 n) (=< n N))))

(forall (n - Integer u - Temporal-unit x - Proper-interval
s - Set)
(if (and (hath n u x)
(forall (y)
(iff (member y s)
(exists (i - Integer)
(and (< 0 i) (=< i n)
(= y (nth-subinterval
i u x)))))))
(concatenation x s)))

;; 4.2-21
(forall (n - Integer u - Temporal-unit x - Proper-interval)
(if (hath n u x)
(int-starts (nth-subinterval 1 u x)
x)))

;; 4.2-23
(forall (n - Integer u - Temporal-unit x - Proper-interval)
(if (hath n u x)
(int-finishes (nth-subinterval n u x)
x)))

;; 4.2-24, 4.2-25
(forall (n - Integer u - Temporal-unit x - Proper-interval)
(if (hath n u x)
(forall (i - Integer)
(if (and (< 0 i) (< i n))
(int-meets (nth-subinterval i u x)
(nth-subinterval (+ i 1) u x))))))

;; 4.3-1
(forall (x y - Proper-interval n - Integer)
(and (iff (wk y n x)
(cal-int y n *week* x))
(iff (wk y n x)
(= (wkFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (wkFn n x)
(nth-subinterval n *week* x)))

;; 4.3-2
(forall (x y - Proper-interval n - Integer)
(if (wk y n x) (week y)))

;;4.3-3
(forall (x y - Proper-interval n - Integer)
(and (iff (dayofweek y n x)
(cal-int y n *day* x))
(iff (dayofweek y n x)
(= (dayofweekFn n x) y))))

(forall (n - Integer x - Proper-interval)
(= (dayofweekFn n x)
(nth-subinterval n *week* x)))

;; 4.3-4
(forall (y x - Proper-interval n - Integer)
(if (dayofweek y n x)
(exists (n1 - Integer x1 - Proper-interval)
(wk x n1 x1))))

;; 4.3-5
(forall (y x - Proper-interval)
(iff (dayofweek y 1 x)
(sunday y x)))

;; 4.3-6
(forall (y x - Proper-interval)
(iff (dayofweek y 2 x)
(monday y x)))

;; 4.3-7
(forall (y x - Proper-interval)
(iff (dayofweek y 3 x)
(tuesday y x)))

;; 4.3-8
(forall (y x - Proper-interval)
(iff (dayofweek y 4 x)
(wednesday y x)))

;; 4.3-9
(forall (y x - Proper-interval)
(iff (dayofweek y 5 x)
(thursday y x)))

;; 4.3-10
(forall (y x - Proper-interval)
(iff (dayofweek y 6 x)
(friday y x)))

;; 4.3-11
(forall (y x - Proper-interval)
(iff (dayofweek y 7 x)
(saturday y x)))

;; 4.3-12
(forall (y - Proper-interval)
(iff (exists (n - Integer x - Proper-interval)
(dayofweek y n x))
(exists (n1 - Integer x1 - Proper-interval)
(da y n1 x1))))

;; 4.3-14
(forall (y x - Proper-interval)
(iff (weekday y x)
(or (monday y x) (tuesday y x) (wednesday y x)
(thursday y x) (friday y x))))

;; 4.3-15
(forall (y x - Proper-interval)
(iff (weekendday y x) (or (saturday y x) (sunday y x))))

;; 4.4-1
(forall (y x - Proper-interval)
(iff (mon y 1 x) (january y x)))

;; 4.4-2
(forall (y x - Proper-interval)
(iff (mon y 2 x) (february y x)))

;; 4.4-3
(forall (y x - Proper-interval)
(iff (mon y 3 x) (march y x)))

;; 4.4-4
(forall (y x - Proper-interval)
(iff (mon y 4 x) (april y x)))

;; 4.4-5
(forall (y x - Proper-interval)
(iff (mon y 5 x) (may y x)))

;; 4.4-6
(forall (y x - Proper-interval)
(iff (mon y 6 x) (june y x)))

;; 4.4-7
(forall (y x - Proper-interval)
(iff (mon y 7 x) (july y x)))

;; 4.4-8
(forall (y x - Proper-interval)
(iff (mon y 8 x) (august y x)))

;; 4.4-9
(forall (y x - Proper-interval)
(iff (mon y 9 x) (september y x)))

;; 4.4-10
(forall (y x - Proper-interval)
(iff (mon y 10 x) (october y x)))

;; 4.4-11
(forall (y x - Proper-interval)
(iff (mon y 11 x) (november y x)))

;; 4.4-12
(forall (y x - Proper-interval)
(iff (mon y 12 x) (december y x)))

;; 4.4-13
(forall (m y - Proper-interval)
(if (january m y) (hath 31 *day* m)))

;; 4.4-14
(forall (m y - Proper-interval)
(if (march m y) (hath 31 *day* m)))

;; 4.4-15
(forall (m y - Proper-interval)
(if (april m y) (hath 30 *day* m)))

;; 4.4-16
(forall (m y - Proper-interval)
(if (may m y) (hath 31 *day* m)))

;; 4.4-17
(forall (m y - Proper-interval)
(if (june m y) (hath 30 *day* m)))

;; 4.4-18
(forall (m y - Proper-interval)
(if (july m y) (hath 31 *day* m)))

;; 4.4-19
(forall (m y - Proper-interval)
(if (august m y) (hath 31 *day* m)))

;; 4.4-20

(forall (m y - Proper-interval)
(if (september m y) (hath 30 *day* m)))

;; 4.4-21
(forall (m y - Proper-interval)
(if (october m y) (hath 31 *day* m)))

;; 4.4-22
(forall (m y - Proper-interval)
(if (november m y) (hath 30 *day* m)))

;; 4.4-23
(forall (m y - Proper-interval)
(if (december m y) (hath 31 *day* m)))

;; 4.4-24
(forall (y - Proper-interval z - Time-standard)
(iff (leap-year y)
(exists (n - Integer)
(and (yr y n (CE z))
(or (divides 400 n)
(and (divides 4 n) (not (divides 100 n))))))))

;; 4.4-25
(forall (m y - Proper-interval)
(if (and (february m y) (leap-year y))
(hath 29 *day* m)))

;; 4.4-26
(forall (m y - Proper-interval)
(if (and (february m y) (not (leap-year y)))
(hath 28 *day* m)))

;; 4.4-27
(forall (int - Proper-interval)
(iff (month int)
(exists (d1 d2 - Proper-interval
n n1 n2 - Integer
m1 m2 y1 y2 e - Proper-interval)
(and (begins-or-in (beginning-of int) d1)
(begins-or-in (end-of int) d2)
(da d1 n m1)
(mon m1 n1 y1)
(yr y1 n2 e)
(da d2 n m2)
(or (mon m2 (+ n1 1) y1)
(exists (y2 - Proper-interval)
(and (= n1 12)
(mon m2 1 y2)
(yr y2 (+ n2 1) e))))))))

;; 4.5-1
(forall (t - Instant
y m d h n s - Integer
z - Time-standard)
(iff (time-of t y m d h n s z)
(begins-or-in t
(secFn
s (minitFn
n (hrFn h (daFn d (monFn m (yrFn y (CE z))))))))))))
```

This archive was generated by hypermail 2.1.4 : 10/21/02 EDT