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