(In-Package "ONTOLINGUA-USER")

;;; Written by user Rse from session "hacking2" owned by group JUST-ME
;;; Date: Oct 27, 1995  15:23


(Define-Ontology
     Simple-Time
     (Frame-Ontology Slot-Constraint-Sugar ranges)
   " A TIME-POINT is a specification of a single point in historical time. CALENDAR-DATE is a time-point at the resolution of days; that is, the day, month, and year are known.  A CALENDAR-YEAR is a time-point at the resolution of years. "
   :Io-Package
   "ONTOLINGUA-USER"
   :Generality
   :high
   :maturity :moderate
   :Issues
   ("Extracted from Bibliographic-Data, October 24, 1995."))


(In-Ontology (Quote Simple-Time))




;;; ------------------ Classes --------------

;;; Calendar-Date

(Define-Class Calendar-Date
              (?T)
              "a specification of a point in absolute calendar time, at the 
resolution of one day."
              :Def
              (And (Time-Point ?T)
               (Has-One ?T Day-of)
               (Has-One ?T Month-of)
               (Has-One ?T Year-of)))


;;; Calendar-Year

(Define-Class Calendar-Year
              (?T)
              "a specification of a point in absolute calendar time, at the 
resolution of one year."
              :Def
              (And (Time-Point ?T)
		   (Has-One ?T Year-of)))


;;; Day-Number

(define-class DAY-NAME (?day)
    "DAY-NAME denotes a name of a day of a week."
    :iff-def (member ?day
		     (setof sunday monday tuesday wednesday thursday
			    friday saturday))
)

(define-individual sunday (day-name))
(define-individual monday (day-name))
(define-individual tuesday (day-name))
(define-individual wednesday (day-name))
(define-individual thursday (day-name))
(define-individual friday (day-name))
(define-individual saturday (day-name))

;;; Month-Name

(Define-Class Month-Name
              (?Month)
              "The months of the year, specified as an extensionally-defined
 (i.e., enumerated) set of objects, in English.
  Instances of this class of months are not symbols, they are months
that may be denoted by object constants."
              :Iff-Def
              (Member ?Month
               (Setof January February March April May June July August
                September October November December))
              :Issues
              (("Why not specify them as an ordered sequence?"
                "The class only defines the set of months.  Their order would
             be given by an ordering predicate: a binary relation.")))


(Define-function Month-number-of (?Month) :-> ?month-number
  "Maps a month to the month-number equivalent."
  :Def (and (month ?month) (month-number ?month-number)))




;;; Time-Point

(Define-Frame Time-Point
              :Own-Slots
              ((Arity 1)
               (Documentation
                "A time-point is a point in real, historical time (on earth).  
It is independent of observer and context.  A time-point is not
a measurement of time, nor is it a specification of time.
It is the point in time. The time-points at which events occur can 
be known with various degrees of precision and approximation,
but conceptually time-points are point-like and not interval-like.
That is, it doesn't make sense to talk about what happens during
a time-point, or how long the time-point lasts.")
               (Domain-Of Day-of Minutes-of Month-of Seconds-of Year-of)
               (Instance-Of Class) (Subclass-Of individual)))




(define-relation EQUALS (?time-point-1 ?time-point-2)
  " a time point ?time-point-1 is equal to a time point ?time-point-2.
    a time range ?time-range-1 is identical to a time range ?time-range-2."
  :axiom-def
  ((=> (and (time-point ?time-point-1) (time-point ?time-point-2))
       (<=> (equals ?time-point-1 ?time-point-2)
	    (and (= (year-of ?time-point-1) (year-of ?time-point-2))
		 (= (month-of ?time-point-1) (month-of ?time-point-2))
		 (= (day-of ?time-point-1) (day-of ?time-point-2))
		 (= (hour-of ?time-point-1) (hour-of ?time-point-2))
		 (= (minute-of ?time-point-1) (minute-of ?time-point-2))
		 (= (second-of ?time-point-1) (second-of ?time-point-2)))))
   (=> (and (time-range ?time-range-1) (time-range ?time-range-2))
       (<=> (EQUALS ?time-range-1 ?time-range-2)
	    (and (equals (START-TIME-OF ?time-range-1)
			 (START-TIME-OF ?time-range-2))
		 (equals (end-time-of ?time-range-1)
			 (end-time-of ?time-range-2)))))))

(define-relation < (?time-point-1 ?time-point-2)
  "a time point ?time-point-1 preceeds a time point ?time-point-2."
  :axiom-def
  (=> (and (time-point ?time-point-1) (time-point ?time-point-2))
      (<=> (< ?time-point-1 ?time-point-2)
	   (or (< (year-of ?time-point-1)
		  (year-of ?time-point-2))
	       (and (= (year-of ?time-point-1)
		       (year-of ?time-point-2))
		    (or (< (month-of ?time-point-1)
			   (month-of ?time-point-2))
			(and (= (month-of ?time-point-1)
				(month-of ?time-point-2))
			     (or (< (day-of ?time-point-1)
				    (day-of ?time-point-2))
				 (and (= (day-of ?time-point-1)
					 (day-of ?time-point-2))
				      (or (< (hour-of ?time-point-1)
					     (hour-of ?time-point-2))
					  (and (= (hour-of ?time-point-1)
						  (hour-of ?time-point-2))
					       (or (< (minute-of ?time-point-1)
						      (minute-of ?time-point-2))
						   (and (= (minute-of
							    ?time-point-1)
							   (minute-of
							    ?time-point-2))
							(or (< (second-of
								?time-point-1)
							       (second-of
								?time-point-2
								))))))))))))))))



(define-relation > (?time-point-1 ?time-point-2)
  "a time point ?time-point-1 preceeds a time point ?time-point-2."
  :axiom-def
  (=> (and (time-point ?time-point-1) (time-point ?time-point-2))
      (<=> (> ?time-point-1 ?time-point-2)
	   (< ?time-point-2 ?time-point-1))))


(define-function MONTH-NAME-of (?time-point) :-> ?month
    "MONTH-OF-NAME denotes a name of a month of a time point."
    :def (and (time-point ?time-point)
	      (month-name ?month))
)

(define-function DAY-of (?time-point) :-> ?day
    "DAY-OF denotes a day of a time point."
    :def (and (time-point ?time-point)
	      (day-number ?day))
)

(define-function DAY-NAME-of (?time-point) :-> ?day
    "DAY-NAME-of denotes a name of a day of a time point."
    :def (and (time-point ?time-point)
	      (day-name ?day))
)

(define-function HOUR-of (?time-point) :-> ?hour
    "HOUR-OF denotes an hour of a time point."
    :def (and (time-point ?time-point)
	      (hour-number ?hour))
)

(define-function MINUTE-of (?time-point) :-> ?minute
    "MINUTE-OF denotes a minute of a time point."
    :def (and (time-point ?time-point)
	      (minute-number ?minute))
)

(define-function SECOND-of (?time-point) :-> ?second
    "TIME-SECOND denotes a second of a time point."	      
    :def (and (time-point ?time-point)
	      (second-number ?second))
)
		      
(define-function UNIT-of (?time-point) :-> ?unit
    "TIME-UNIT denotes a unit of a time point."
    :def (and (time-point ?time-point)
	      (duration ?unit))
)


;;; Year-Number

(Define-Class Year-Number
              (?Year)
              "A year expressed as the number of years A.D."
              :Def
              (Integer ?Year))



;;; ------------------ Relations --------------


;;; ------------------ Functions --------------

;;; Day

;;; Minutes

(Define-Function Minutes-of
                 (?Time-Point)
                 :->
                 ?Minutes
                 "function from time points to integers representing the minutes
component of the time specification."
                 :Def
                 (And (Time-Point ?Time-Point) (Integer ?Minutes)
                  (=< 0 ?Minutes) (=< ?Minutes 59)))


;;; Month

(Define-Function Month-of
                 (?Time-Point)
                 :->
                 ?Month
                 "function from time points to months, representing the month component of
the time specification.  Months are not integers, but named objects."
                 :Def
                 (And (Time-Point ?Time-Point) (Month-Name ?Month)))


;;; Seconds

(Define-Function Seconds-of
                 (?Time-Point)
                 :->
                 ?Seconds
                 "function from time points to integers representing the seconds component of
the time specification.  This is not the internal representation of the
universal time, (e.g., number seconds since some historical date).
seconds is the number of seconds past the minute, hour, day, etc.
specified in the other components of the "
                 :Def
                 (And (Time-Point ?Time-Point) (Integer ?Seconds)
                  (=< 0 ?Seconds) (=< ?Seconds 59)))


;;; Year

(Define-Function Year-of
                 (?Time-Point)
                 :->
                 ?Year
                 "function from time points to integers representing the year
component of the time specification.  The integer represents
the number of years A.D., e.g., 1992."
                 :Def
                 (And (Time-Point ?Time-Point) (Year-Number ?Year)))



(define-class MONTH-NUMBER (?month)
    "MONTH-NUMBER deontes a month of a year."
    :axiom-def (and (integer-range month-number)
		    (= (i-lower-bound month-number) 1)
		    (= (i-upper-bound month-number) 12))
)

(define-individual 1-the-month-number (month-number)
  :axiom-def (pretty-name 1-the-month-number "1")
  := 1)

(define-individual 2-the-month-number (month-number)
  :axiom-def (pretty-name 2-the-month-number "2")
  := 2)

(define-individual 3-the-month-number (month-number)
  :axiom-def (pretty-name 3-the-month-number "3")
  := 3)

(define-individual 4-the-month-number (month-number)
  :axiom-def (pretty-name 4-the-month-number "4")
  := 4)

(define-individual 5-the-month-number (month-number)
  :axiom-def (pretty-name 5-the-month-number "5")
  := 5)

(define-individual 6-the-month-number (month-number)
  :axiom-def (pretty-name 6-the-month-number "6")
  := 6)

(define-individual 7-the-month-number (month-number)
  :axiom-def (pretty-name 7-the-month-number "7")
  := 7)

(define-individual 8-the-month-number (month-number)
  :axiom-def (pretty-name 8-the-month-number "8")
  := 8)

(define-individual 9-the-month-number (month-number)
  :axiom-def (pretty-name 9-the-month-number "9")
  := 9)

(define-individual 10-the-month-number (month-number)
  :axiom-def (pretty-name 10-the-month-number "10")
  := 10)

(define-individual 11-the-month-number (month-number)
  :axiom-def (pretty-name 11-the-month-number "11")
  := 11)

(define-individual 12-the-month-number (month-number)
  :axiom-def (pretty-name 12-the-month-number "12")
  := 12)

(define-class DAY-NUMBER (?day)
    "DAY-NUMBER denotes a day of a month."
    :axiom-def (and (integer-range day-number)
		    (= (i-lower-bound day-number) 1)
		    (= (i-upper-bound day-number) 31))
)

(define-individual 1-the-day-number (day-number)
  :axiom-def (pretty-name 1-the-day-number "1")
  := 1)

(define-individual 2-the-day-number (day-number)
  :axiom-def (pretty-name 2-the-day-number "2")
  := 2)

(define-individual 3-the-day-number (day-number)
  :axiom-def (pretty-name 3-the-day-number "3")
  := 3)

(define-individual 4-the-day-number (day-number)
  :axiom-def (pretty-name 4-the-day-number "4")
  := 4)

(define-individual 5-the-day-number (day-number)
  :axiom-def (pretty-name 5-the-day-number "5")
  := 5)

(define-individual 6-the-day-number (day-number)
  :axiom-def (pretty-name 6-the-day-number "6")
  := 6)

(define-individual 7-the-day-number (day-number)
  :axiom-def (pretty-name 7-the-day-number "7")
  := 7)

(define-individual 8-the-day-number (day-number)
  :axiom-def (pretty-name 8-the-day-number "8")
  := 8)

(define-individual 9-the-day-number (day-number)
  :axiom-def (pretty-name 9-the-day-number "9")
  := 9)

(define-individual 10-the-day-number (day-number)
  :axiom-def (pretty-name 10-the-day-number "10")
  := 10)

(define-individual 11-the-day-number (day-number)
  :axiom-def (pretty-name 11-the-day-number "11")
  := 11)

(define-individual 12-the-day-number (day-number)
  :axiom-def (pretty-name 12-the-day-number "12")
  := 12)

(define-individual 13-the-day-number (day-number)
  :axiom-def (pretty-name 13-the-day-number "13")
  := 13)

(define-individual 14-the-day-number (day-number)
  :axiom-def (pretty-name 14-the-day-number "14")
  := 14)

(define-individual 15-the-day-number (day-number)
  :axiom-def (pretty-name 15-the-day-number "15")
  := 15)

(define-individual 16-the-day-number (day-number)
  :axiom-def (pretty-name 16-the-day-number "16")
  := 16)

(define-individual 17-the-day-number (day-number)
  :axiom-def (pretty-name 17-the-day-number "17")
  := 17)

(define-individual 18-the-day-number (day-number)
  :axiom-def (pretty-name 18-the-day-number "18")
  := 18)

(define-individual 19-the-day-number (day-number)
  :axiom-def (pretty-name 19-the-day-number "19")
  := 19)

(define-individual 20-the-day-number (day-number)
  :axiom-def (pretty-name 20-the-day-number "20")
  := 20)

(define-individual 21-the-day-number (day-number)
  :axiom-def (pretty-name 21-the-day-number "21")
  := 21)

(define-individual 22-the-day-number (day-number)
  :axiom-def (pretty-name 22-the-day-number "22")
  := 22)

(define-individual 23-the-day-number (day-number)
  :axiom-def (pretty-name 23-the-day-number "23")
  := 23)

(define-individual 24-the-day-number (day-number)
  :axiom-def (pretty-name 24-the-day-number "24")
  := 24)

(define-individual 25-the-day-number (day-number)
  :axiom-def (pretty-name 25-the-day-number "25")
  := 25)

(define-individual 26-the-day-number (day-number)
  :axiom-def (pretty-name 26-the-day-number "26")
  := 26)

(define-individual 27-the-day-number (day-number)
  :axiom-def (pretty-name 27-the-day-number "27")
  := 27)

(define-individual 28-the-day-number (day-number)
  :axiom-def (pretty-name 28-the-day-number "28")
  := 28)

(define-individual 29-the-day-number (day-number)
  :axiom-def (pretty-name 29-the-day-number "29")
  := 29)

(define-individual 30-the-day-number (day-number)
  :axiom-def (pretty-name 30-the-day-number "30")
  := 30)

(define-individual 31-the-day-number (day-number)
  :axiom-def (pretty-name 31-the-day-number "31")
  := 31)


(define-class HOUR-NUMBER (?hour)
    "HOUR-NUMBER denotes an hour of a day."
    :axiom-def (and (integer-range hour-number)
		    (= (i-lower-bound hour-number) 0)
		    (= (i-upper-bound hour-number) 23))
)

(define-individual 0-the-hour-number (hour-number)
  :axiom-def (pretty-name 0-the-hour-number "0")
  := 0)

(define-individual 1-the-hour-number (hour-number)
  :axiom-def (pretty-name 1-the-hour-number "1")
  := 1)

(define-individual 2-the-hour-number (hour-number)
  :axiom-def (pretty-name 2-the-hour-number "2")
  := 2)

(define-individual 3-the-hour-number (hour-number)
  :axiom-def (pretty-name 3-the-hour-number "3")
  := 3)

(define-individual 4-the-hour-number (hour-number)
  :axiom-def (pretty-name 4-the-hour-number "4")
  := 4)

(define-individual 5-the-hour-number (hour-number)
  :axiom-def (pretty-name 5-the-hour-number "5")
  := 5)

(define-individual 6-the-hour-number (hour-number)
  :axiom-def (pretty-name 6-the-hour-number "6")
  := 6)

(define-individual 7-the-hour-number (hour-number)
  :axiom-def (pretty-name 7-the-hour-number "7")
  := 7)

(define-individual 8-the-hour-number (hour-number)
  :axiom-def (pretty-name 8-the-hour-number "8")
  := 8)

(define-individual 9-the-hour-number (hour-number)
  :axiom-def (pretty-name 9-the-hour-number "9")
  := 9)

(define-individual 10-the-hour-number (hour-number)
  :axiom-def (pretty-name 10-the-hour-number "10")
  := 10)

(define-individual 11-the-hour-number (hour-number)
  :axiom-def (pretty-name 11-the-hour-number "11")
  := 11)

(define-individual 12-the-hour-number (hour-number)
  :axiom-def (pretty-name 12-the-hour-number "12")
  := 12)

(define-individual 13-the-hour-number (hour-number)
  :axiom-def (pretty-name 13-the-hour-number "13")
  := 13)

(define-individual 14-the-hour-number (hour-number)
  :axiom-def (pretty-name 14-the-hour-number "14")
  := 14)

(define-individual 15-the-hour-number (hour-number)
  :axiom-def (pretty-name 15-the-hour-number "15")
  := 15)

(define-individual 16-the-hour-number (hour-number)
  :axiom-def (pretty-name 16-the-hour-number "16")
  := 16)

(define-individual 17-the-hour-number (hour-number)
  :axiom-def (pretty-name 17-the-hour-number "17")
  := 17)

(define-individual 18-the-hour-number (hour-number)
  :axiom-def (pretty-name 18-the-hour-number "18")
  := 18)

(define-individual 19-the-hour-number (hour-number)
  :axiom-def (pretty-name 19-the-hour-number "19")
  := 19)

(define-individual 20-the-hour-number (hour-number)
  :axiom-def (pretty-name 20-the-hour-number "20")
  := 20)

(define-individual 21-the-hour-number (hour-number)
  :axiom-def (pretty-name 21-the-hour-number "21")
  := 21)

(define-individual 22-the-hour-number (hour-number)
  :axiom-def (pretty-name 22-the-hour-number "22")
  := 22)

(define-individual 23-the-hour-number (hour-number)
  :axiom-def (pretty-name 23-the-hour-number "23")
  := 23)


(define-class MINUTE-NUMBER (?minute)
    "MINUTE-NUMBER denotes a minute of a hour."
    :axiom-def (and (integer-range minute-number)
		    (= (i-lower-bound minute-number) 0)
		    (= (i-upper-bound minute-number) 59))
)

(define-individual 0-the-minute-number (minute-number)
  :axiom-def (pretty-name 0-the-minute-number "0")
  := 0)

(define-individual 1-the-minute-number (minute-number)
  :axiom-def (pretty-name 1-the-minute-number "1")
  := 1)

(define-individual 2-the-minute-number (minute-number)
  :axiom-def (pretty-name 2-the-minute-number "2")
  := 2)

(define-individual 3-the-minute-number (minute-number)
  :axiom-def (pretty-name 3-the-minute-number "3")
  := 3)

(define-individual 4-the-minute-number (minute-number)
  :axiom-def (pretty-name 4-the-minute-number "4")
  := 4)

(define-individual 5-the-minute-number (minute-number)
  :axiom-def (pretty-name 5-the-minute-number "5")
  := 5)

(define-individual 6-the-minute-number (minute-number)
  :axiom-def (pretty-name 6-the-minute-number "6")
  := 6)

(define-individual 7-the-minute-number (minute-number)
  :axiom-def (pretty-name 7-the-minute-number "7")
  := 7)

(define-individual 8-the-minute-number (minute-number)
  :axiom-def (pretty-name 8-the-minute-number "8")
  := 8)

(define-individual 9-the-minute-number (minute-number)
  :axiom-def (pretty-name 9-the-minute-number "9")
  := 9)

(define-individual 10-the-minute-number (minute-number)
  :axiom-def (pretty-name 10-the-minute-number "10")
  := 10)

(define-individual 11-the-minute-number (minute-number)
  :axiom-def (pretty-name 11-the-minute-number "11")
  := 11)

(define-individual 12-the-minute-number (minute-number)
  :axiom-def (pretty-name 12-the-minute-number "12")
  := 12)

(define-individual 13-the-minute-number (minute-number)
  :axiom-def (pretty-name 13-the-minute-number "13")
  := 13)

(define-individual 14-the-minute-number (minute-number)
  :axiom-def (pretty-name 14-the-minute-number "14")
  := 14)

(define-individual 15-the-minute-number (minute-number)
  :axiom-def (pretty-name 15-the-minute-number "15")
  := 15)

(define-individual 16-the-minute-number (minute-number)
  :axiom-def (pretty-name 16-the-minute-number "16")
  := 16)

(define-individual 17-the-minute-number (minute-number)
  :axiom-def (pretty-name 17-the-minute-number "17")
  := 17)

(define-individual 18-the-minute-number (minute-number)
  :axiom-def (pretty-name 18-the-minute-number "18")
  := 18)

(define-individual 19-the-minute-number (minute-number)
  :axiom-def (pretty-name 19-the-minute-number "19")
  := 19)

(define-individual 20-the-minute-number (minute-number)
  :axiom-def (pretty-name 20-the-minute-number "20")
  := 20)

(define-individual 21-the-minute-number (minute-number)
  :axiom-def (pretty-name 21-the-minute-number "21")
  := 21)

(define-individual 22-the-minute-number (minute-number)
  :axiom-def (pretty-name 22-the-minute-number "22")
  := 22)

(define-individual 23-the-minute-number (minute-number)
  :axiom-def (pretty-name 23-the-minute-number "23")
  := 23)

(define-individual 24-the-minute-number (minute-number)
  :axiom-def (pretty-name 24-the-minute-number "24")
  := 24)

(define-individual 25-the-minute-number (minute-number)
  :axiom-def (pretty-name 25-the-minute-number "25")
  := 25)

(define-individual 26-the-minute-number (minute-number)
  :axiom-def (pretty-name 26-the-minute-number "26")
  := 26)

(define-individual 27-the-minute-number (minute-number)
  :axiom-def (pretty-name 27-the-minute-number "27")
  := 27)

(define-individual 28-the-minute-number (minute-number)
  :axiom-def (pretty-name 28-the-minute-number "28")
  := 28)

(define-individual 29-the-minute-number (minute-number)
  :axiom-def (pretty-name 29-the-minute-number "29")
  := 29)

(define-individual 30-the-minute-number (minute-number)
  :axiom-def (pretty-name 30-the-minute-number "30")
  := 30)

(define-individual 31-the-minute-number (minute-number)
  :axiom-def (pretty-name 31-the-minute-number "31")
  := 31)

(define-individual 32-the-minute-number (minute-number)
  :axiom-def (pretty-name 32-the-minute-number "32")
  := 32)

(define-individual 33-the-minute-number (minute-number)
  :axiom-def (pretty-name 33-the-minute-number "33")
  := 33)

(define-individual 34-the-minute-number (minute-number)
  :axiom-def (pretty-name 34-the-minute-number "34")
  := 34)

(define-individual 35-the-minute-number (minute-number)
  :axiom-def (pretty-name 35-the-minute-number "35")
  := 35)

(define-individual 36-the-minute-number (minute-number)
  :axiom-def (pretty-name 36-the-minute-number "36")
  := 36)

(define-individual 37-the-minute-number (minute-number)
  :axiom-def (pretty-name 37-the-minute-number "37")
  := 37)

(define-individual 38-the-minute-number (minute-number)
  :axiom-def (pretty-name 38-the-minute-number "38")
  := 38)

(define-individual 39-the-minute-number (minute-number)
  :axiom-def (pretty-name 39-the-minute-number "39")
  := 39)

(define-individual 40-the-minute-number (minute-number)
  :axiom-def (pretty-name 40-the-minute-number "40")
  := 40)

(define-individual 41-the-minute-number (minute-number)
  :axiom-def (pretty-name 41-the-minute-number "41")
  := 41)

(define-individual 42-the-minute-number (minute-number)
  :axiom-def (pretty-name 42-the-minute-number "42")
  := 42)

(define-individual 43-the-minute-number (minute-number)
  :axiom-def (pretty-name 43-the-minute-number "43")
  := 43)

(define-individual 44-the-minute-number (minute-number)
  :axiom-def (pretty-name 44-the-minute-number "44")
  := 44)

(define-individual 45-the-minute-number (minute-number)
  :axiom-def (pretty-name 45-the-minute-number "45")
  := 45)

(define-individual 46-the-minute-number (minute-number)
  :axiom-def (pretty-name 46-the-minute-number "46")
  := 46)

(define-individual 47-the-minute-number (minute-number)
  :axiom-def (pretty-name 47-the-minute-number "47")
  := 47)

(define-individual 48-the-minute-number (minute-number)
  :axiom-def (pretty-name 48-the-minute-number "48")
  := 48)

(define-individual 49-the-minute-number (minute-number)
  :axiom-def (pretty-name 49-the-minute-number "49")
  := 49)

(define-individual 50-the-minute-number (minute-number)
  :axiom-def (pretty-name 50-the-minute-number "50")
  := 50)

(define-individual 51-the-minute-number (minute-number)
  :axiom-def (pretty-name 51-the-minute-number "51")
  := 51)

(define-individual 52-the-minute-number (minute-number)
  :axiom-def (pretty-name 52-the-minute-number "52")
  := 52)

(define-individual 53-the-minute-number (minute-number)
  :axiom-def (pretty-name 53-the-minute-number "53")
  := 53)

(define-individual 54-the-minute-number (minute-number)
  :axiom-def (pretty-name 54-the-minute-number "54")
  := 54)

(define-individual 55-the-minute-number (minute-number)
  :axiom-def (pretty-name 55-the-minute-number "55")
  := 55)

(define-individual 56-the-minute-number (minute-number)
  :axiom-def (pretty-name 56-the-minute-number "56")
  := 56)

(define-individual 57-the-minute-number (minute-number)
  :axiom-def (pretty-name 57-the-minute-number "57")
  := 57)

(define-individual 58-the-minute-number (minute-number)
  :axiom-def (pretty-name 58-the-minute-number "58")
  := 58)

(define-individual 59-the-minute-number (minute-number)
  :axiom-def (pretty-name 59-the-minute-number "59")
  := 59)


(define-class SECOND-NUMBER (?second)
    "SECOND-NUMBER denotes a second of a minute."
    :axiom-def (and (real-range second-number)
		    (= (r-lower-bound second-number) 0)
		    (= (r-upper-bound second-number) 59))
)

(define-individual 0-the-second-number (second-number)
  :axiom-def (pretty-name 0-the-second-number "0")
  := 0)

(define-individual 1-the-second-number (second-number)
  :axiom-def (pretty-name 1-the-second-number "1")
  := 1)

(define-individual 2-the-second-number (second-number)
  :axiom-def (pretty-name 2-the-second-number "2")
  := 2)

(define-individual 3-the-second-number (second-number)
  :axiom-def (pretty-name 3-the-second-number "3")
  := 3)

(define-individual 4-the-second-number (second-number)
  :axiom-def (pretty-name 4-the-second-number "4")
  := 4)

(define-individual 5-the-second-number (second-number)
  :axiom-def (pretty-name 5-the-second-number "5")
  := 5)

(define-individual 6-the-second-number (second-number)
  :axiom-def (pretty-name 6-the-second-number "6")
  := 6)

(define-individual 7-the-second-number (second-number)
  :axiom-def (pretty-name 7-the-second-number "7")
  := 7)

(define-individual 8-the-second-number (second-number)
  :axiom-def (pretty-name 8-the-second-number "8")
  := 8)

(define-individual 9-the-second-number (second-number)
  :axiom-def (pretty-name 9-the-second-number "9")
  := 9)

(define-individual 10-the-second-number (second-number)
  :axiom-def (pretty-name 10-the-second-number "10")
  := 10)

(define-individual 11-the-second-number (second-number)
  :axiom-def (pretty-name 11-the-second-number "11")
  := 11)

(define-individual 12-the-second-number (second-number)
  :axiom-def (pretty-name 12-the-second-number "12")
  := 12)

(define-individual 13-the-second-number (second-number)
  :axiom-def (pretty-name 13-the-second-number "13")
  := 13)

(define-individual 14-the-second-number (second-number)
  :axiom-def (pretty-name 14-the-second-number "14")
  := 14)

(define-individual 15-the-second-number (second-number)
  :axiom-def (pretty-name 15-the-second-number "15")
  := 15)

(define-individual 16-the-second-number (second-number)
  :axiom-def (pretty-name 16-the-second-number "16")
  := 16)

(define-individual 17-the-second-number (second-number)
  :axiom-def (pretty-name 17-the-second-number "17")
  := 17)

(define-individual 18-the-second-number (second-number)
  :axiom-def (pretty-name 18-the-second-number "18")
  := 18)

(define-individual 19-the-second-number (second-number)
  :axiom-def (pretty-name 19-the-second-number "19")
  := 19)

(define-individual 20-the-second-number (second-number)
  :axiom-def (pretty-name 20-the-second-number "20")
  := 20)

(define-individual 21-the-second-number (second-number)
  :axiom-def (pretty-name 21-the-second-number "21")
  := 21)

(define-individual 22-the-second-number (second-number)
  :axiom-def (pretty-name 22-the-second-number "22")
  := 22)

(define-individual 23-the-second-number (second-number)
  :axiom-def (pretty-name 23-the-second-number "23")
  := 23)

(define-individual 24-the-second-number (second-number)
  :axiom-def (pretty-name 24-the-second-number "24")
  := 24)

(define-individual 25-the-second-number (second-number)
  :axiom-def (pretty-name 25-the-second-number "25")
  := 25)

(define-individual 26-the-second-number (second-number)
  :axiom-def (pretty-name 26-the-second-number "26")
  := 26)

(define-individual 27-the-second-number (second-number)
  :axiom-def (pretty-name 27-the-second-number "27")
  := 27)

(define-individual 28-the-second-number (second-number)
  :axiom-def (pretty-name 28-the-second-number "28")
  := 28)

(define-individual 29-the-second-number (second-number)
  :axiom-def (pretty-name 29-the-second-number "29")
  := 29)

(define-individual 30-the-second-number (second-number)
  :axiom-def (pretty-name 30-the-second-number "30")
  := 30)

(define-individual 31-the-second-number (second-number)
  :axiom-def (pretty-name 31-the-second-number "31")
  := 31)

(define-individual 32-the-second-number (second-number)
  :axiom-def (pretty-name 32-the-second-number "32")
  := 32)

(define-individual 33-the-second-number (second-number)
  :axiom-def (pretty-name 33-the-second-number "33")
  := 33)

(define-individual 34-the-second-number (second-number)
  :axiom-def (pretty-name 34-the-second-number "34")
  := 34)

(define-individual 35-the-second-number (second-number)
  :axiom-def (pretty-name 35-the-second-number "35")
  := 35)

(define-individual 36-the-second-number (second-number)
  :axiom-def (pretty-name 36-the-second-number "36")
  := 36)

(define-individual 37-the-second-number (second-number)
  :axiom-def (pretty-name 37-the-second-number "37")
  := 37)

(define-individual 38-the-second-number (second-number)
  :axiom-def (pretty-name 38-the-second-number "38")
  := 38)

(define-individual 39-the-second-number (second-number)
  :axiom-def (pretty-name 39-the-second-number "39")
  := 39)

(define-individual 40-the-second-number (second-number)
  :axiom-def (pretty-name 40-the-second-number "40")
  := 40)

(define-individual 41-the-second-number (second-number)
  :axiom-def (pretty-name 41-the-second-number "41")
  := 41)

(define-individual 42-the-second-number (second-number)
  :axiom-def (pretty-name 42-the-second-number "42")
  := 42)

(define-individual 43-the-second-number (second-number)
  :axiom-def (pretty-name 43-the-second-number "43")
  := 43)

(define-individual 44-the-second-number (second-number)
  :axiom-def (pretty-name 44-the-second-number "44")
  := 44)

(define-individual 45-the-second-number (second-number)
  :axiom-def (pretty-name 45-the-second-number "45")
  := 45)

(define-individual 46-the-second-number (second-number)
  :axiom-def (pretty-name 46-the-second-number "46")
  := 46)

(define-individual 47-the-second-number (second-number)
  :axiom-def (pretty-name 47-the-second-number "47")
  := 47)

(define-individual 48-the-second-number (second-number)
  :axiom-def (pretty-name 48-the-second-number "48")
  := 48)

(define-individual 49-the-second-number (second-number)
  :axiom-def (pretty-name 49-the-second-number "49")
  := 49)

(define-individual 50-the-second-number (second-number)
  :axiom-def (pretty-name 50-the-second-number "50")
  := 50)

(define-individual 51-the-second-number (second-number)
  :axiom-def (pretty-name 51-the-second-number "51")
  := 51)

(define-individual 52-the-second-number (second-number)
  :axiom-def (pretty-name 52-the-second-number "52")
  := 52)

(define-individual 53-the-second-number (second-number)
  :axiom-def (pretty-name 53-the-second-number "53")
  := 53)

(define-individual 54-the-second-number (second-number)
  :axiom-def (pretty-name 54-the-second-number "54")
  := 54)

(define-individual 55-the-second-number (second-number)
  :axiom-def (pretty-name 55-the-second-number "55")
  := 55)

(define-individual 56-the-second-number (second-number)
  :axiom-def (pretty-name 56-the-second-number "56")
  := 56)

(define-individual 57-the-second-number (second-number)
  :axiom-def (pretty-name 57-the-second-number "57")
  := 57)

(define-individual 58-the-second-number (second-number)
  :axiom-def (pretty-name 58-the-second-number "58")
  := 58)

(define-individual 59-the-second-number (second-number)
  :axiom-def (pretty-name 59-the-second-number "59")
  := 59)

;;; ------------------ Instance --------------

;;; January

(Define-Individual January (Month-Name)
  :axiom-def (Month-number-of january 1-the-month-number))


;;; February

(Define-Individual February (Month-Name)
  :axiom-def (Month-number-of february 2-the-month-number))


;;; March

(Define-Individual March (Month-Name)
  :axiom-def (Month-number-of march 3-the-month-number))


;;; April

(Define-Individual April (Month-Name)
  :axiom-def (Month-number-of april 4-the-month-number))


;;; May

(Define-Individual May (Month-Name)
  :axiom-def (Month-number-of may 5-the-month-number))


;;; June

(Define-Individual June (Month-Name)
  :axiom-def (Month-number-of june 6-the-month-number))


;;; July

(Define-Individual July (Month-Name)
  :axiom-def (Month-number-of july 7-the-month-number))


;;; August

(Define-Individual August (Month-Name)
  :axiom-def (Month-number-of august 8-the-month-number))


;;; September

(Define-Individual September (Month-Name)
  :axiom-def (Month-number-of september 9-the-month-number))


;;; October

(Define-Individual October (Month-Name)
  :axiom-def (Month-number-of october 10-the-month-number))


;;; November

(Define-Individual November (Month-Name)
  :axiom-def (Month-number-of november 11-the-month-number))


;;; December

(Define-Individual December (Month-Name)
  :axiom-def (Month-number-of december 12-the-month-number))




;;; ------------------ Axiom --------------


;;; ------------------ Other --------------


(define-class TIME-RANGE (?time-range) 
    "TIME-RANGE denotes a certain period of time. It consists of a
start time, an end time. A start time must proceed an end time.
Relations between TIME-RANGEs are defined after James Allen's interval
relations."
    :def (individual ?time-range)
    :constraints (equals  (+ (START-TIME-OF ?time-range)
			    (duration-of ?time-range))
		       (end-time-of ?time-range))
)

(define-function START-TIME-OF (?time-range) :-> ?time-point
    "(START-TIME-OF 'tr) denotes a start time of a time range tr."
    :def (and (time-range ?time-range)
	      (time-point ?time-point))
)

(define-function END-TIME-OF (?time-range) :-> ?time-point
    "(END-TIME-OF 'tr) denotes an end time of a time range tr."
    :def (and (time-range ?time-range)
	      (time-point ?time-point))
)

(define-function DURATION-OF (?time-range) :-> ?duration
    "(DURATION-OF 'tr) denotes a duration of a time range tr."
    :def (and (time-range ?time-range)
	      (duration ?duration))
)

(define-relation BEFORE (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 preceeds a time ranage ?time-range-2."
  :iff-def (< (end-time-of ?time-range-1)
		  (START-TIME-OF ?time-range-2))
)

(define-relation AFTER (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 succeeds a time range ?time-range-2."
    :iff-def (< (end-time-of ?time-range-2)
		  (START-TIME-OF ?time-range-1))
    :equivalent (before ?time-range-2 ?time-range-1)
)

(define-relation MEETS (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 ends at the same time a time range
     ?time-range-2 starts."
    :iff-def (equals (end-time-of ?time-range-1)
		  (START-TIME-OF ?time-range-2))
)		 



(define-relation DURING (?time-range-1 ?time-range-2)
  "a time range ?time-range-1 is properly included in a time range
   ?time-range-2."
  :iff-def (and (> (START-TIME-OF ?time-range-1)
		   (START-TIME-OF ?time-range-2))
		(< (end-time-of ?time-range-1)
		   (end-time-of ?time-range-2)))
)

(define-relation OVERLAPS (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 and a time range ?time-range-2 overlaps."
    :iff-def (and (< (START-TIME-OF ?time-range-1)
		     (START-TIME-OF ?time-range-2))
		  (< (START-TIME-OF ?time-range-2)
		     (end-time-of ?time-range-1))
		  (< (end-time-of ?time-range-1)
		     (end-time-of ?time-range-2)))
)

(define-relation STARTS (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 and a time range ?time-range-2 starts at the
     same time and a duration of ?time-range-1 is shorter than that of
     ?time-range-2."
    :iff-def (and (equals (START-TIME-OF ?time-range-1)
		       (START-TIME-OF ?time-range-2))
		  (< (end-time-of ?time-range-1)
		     (end-time-of ?time-range-2)))
)

(define-relation FINISHES (?time-range-1 ?time-range-2)
    "a time range ?time-range-1 and a time range ?time-range-2 ends at the
     same time and a duration of ?time-range-1 is shorter than that of
     ?time-range-2."
    :iff-def (and (> (START-TIME-OF ?time-range-1)
		     (START-TIME-OF ?time-range-2))
		  (equals (end-time-of ?time-range-1)
			  (end-time-of ?time-range-2)))
)

(define-relation BEFORE= (?time-range-1 ?time-range-2)
    :iff-def (or (before ?time-range-1 ?time-range-2)
		 (meets ?time-range-1 ?time-range-2))
)

(define-relation AFTER= (?time-range-1 ?time-range-2)
    :iff-def (or (after ?time-range-1 ?time-range-2)
		 (meets ?time-range-2 ?time-range-1))
)

(define-relation DURING= (?time-range-1 ?time-range-2)
    :iff-def (or (during ?time-range-1 ?time-range-2)
		 (starts ?time-range-1 ?time-range-2)
		 (finishes ?time-range-1 ?time-range-2)
		 (equals ?time-range-1 ?time-range-2))
)

(define-relation OVERLAPS= (?time-range-1 ?time-range-2)
    :iff-def (or (overlaps ?time-range-1 ?time-range-2)
		 (meets ?time-range-1 ?time-range-2))
)

(define-relation START= (?time-range-1 ?time-range-2)
    :iff-def (or (starts ?time-range-1 ?time-range-2)
		 (equals ?time-range-1 ?time-range-2))
)

(define-relation FINISHES= (?time-range-1 ?time-range-2)
    :iff-def (or (finishes ?time-range-1 ?time-range-2)
		 (equals ?time-range-1 ?time-range-2))
)

(define-relation DISJOINT-TIME-RANGES (?time-range-1 ?time-range-2)
    "time ranges ?time-range-1 and ?time-range-2 do not overlap"
    :iff-def (or (before ?time-range-1 ?time-range-2)
		 (before ?time-range-2 ?time-range-1)))

(define-function + (?time-range-1 ?duration) :-> ?time-range-2
    "+ denotes a time range ?time-range-2 whose length is longer
     that ?time-range-1 by a duration ?duration.
     A difference between two time points ?time-point-1 and ?time-point-2 is a
     duration ?duration."
  :axiom-def
  ((=> (and (time-range ?time-range-1)
	     (duration ?duration))
	(<=> (= (+ ?time-range-1 ?duration) ?time-range-2)
	     (and (= (START-TIME-OF ?time-range-1)
		     (START-TIME-OF ?time-range-2))
		  (= (+ (end-time-of ?time-range-1) ?duration)
		     (end-time-of ?time-range-2)))))
   (=> (and (time-point ?time-range-1)
	   (duration ?duration))
      (=> (= (+ ?time-point-1 ?duration) ?time-point-2)
	  (and (time-point ?time-point-1)
	       (duration ?duration)
	       (time-point ?time-point-2))))
   (=> (and (duration ?duration-1) (duration ?duration-2))
       (=> (= (+ ?duration-1 ?duration-2) ?duration-3)
	   (duration ?duration-3)))))


;==============================================================================


(define-class DURATION (?duration)
    "DURATION denotes a period of time. It consists of a value and a
     measure"
    :def (individual ?duration))

(define-function VALUE-OF (?duration) :-> ?value
    "VALUE-OF returns a length of a duration in a cetain measure."
    :def (and (duration ?duration)
	      (integer ?value)))

;;; Universal-Time-Spec

(Define-Class Universal-Time-Spec
              (?T)
  "a specification of a point in real-world, historical, wall-clock time,
   independent of timezone and with one second resolution."
              :Def (And (Time-Point ?T) (Has-One ?T seconds-of)
			(Has-One ?T minutes-of) (Has-One ?T day-of)
			(Has-One ?T month-of) (Has-One ?T year-of)))