Revised daml-time.pddl

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

  • Next message: pat hayes: "Re: Further remarks"
    I forgot two things in my previous message:
    
    1) Yoav Shoham worked out an exhaustive taxonomy of eventuality types
       as part of his Ph.D. work.  Different types behave differently with
       regard to whether holding over an interval implies holding at each
       instant of the interval, and other such distinctions.  I'm not sure
       where to find the taxonomy, but we could ask Yoav.
    
    2) Here's the revised PDDL version of daml-time:
    
    ;;; 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)
    
          (holds e - Eventuality ti - Temporal-entity)
          (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)
    	  (if (not (= t1 *PosInf*))
    	      (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)
    	  (if (not (= t1 *NegInf*))
    	      (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)))
    
           (forall (e - Eventuality ti - Instant)
    	  (iff (holds e ti)
    	       (at-time e ti)))
    
           (forall (e - Eventuality ti - Interval)
    	  (iff (holds e ti)
    	       (during 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 - 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
           ;; These all imply that y and x are "official" days, hours, or
           ;; whatever.
           (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)))
    
           ;; Revised 4.3-3,4:
           (forall (y x - Proper-interval n - Integer)
    	  (iff (dayofweek y n x)
    	       (exists (n1 - Integer x1 - Proper-interval)
    		  (and (wk x n1 x1)
    		       (cal-int y n *day* 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/29/02 EST