;;; Mode: Lisp; Package: ocml

;;; The Open University

(in-package "OCML")

;;;A minimalist set of time-related definitions. 
;;;We may want to extend this in the future

(in-ontology akt-support-ontology)

(def-class YEAR-IN-TIME (integer) ?x
	"A year-in-time must be an integer and integer can be a year-in-time"
	:iff-def (integer ?x)
        :avoid-infinite-loop t)

(def-class MONTH-IN-TIME (positive-integer)?x
	"A month-in-time is an integer in the interval 1-12"
	:iff-def (and (positive-integer ?x)(< ?x 13) )
        :avoid-infinite-loop t)

(def-class DAY-IN-TIME (positive-integer)?x
	"A day-in-time is an integer in the interval 1-31"
	:iff-def (and (positive-integer ?x)(< ?x 32) )
        :avoid-infinite-loop t)

(def-class HOUR-IN-TIME (non-negative-integer)?x
	"A hour-in-time is an integer in the interval 0-23"
	:iff-def (and (non-negative-integer ?x)(< ?x 24) )
        :avoid-infinite-loop t)

(def-class MINUTE-IN-TIME (non-negative-integer) ?x
	"A minute-in-time is an integer in the interval 0-59"
	:iff-def (and (non-negative-integer ?x)(< ?x 60) )
        :avoid-infinite-loop t)

(def-class SECOND-IN-TIME (non-negative-integer)?x
	"A second-in-time is an integer in the interval 0-59"
	:iff-def (and (non-negative-integer ?x)(< ?x 60) )
        :avoid-infinite-loop t)


(def-class TIME-ENTITY (intangible-thing)
  "WARNING: The constraint below ought to be extended to handle leap years.
   We use this generic notion of time entity which subsumes both time intervals
   and time points"
  ((minute-of :type minute-in-time :max-cardinality 1 )
   (second-of :type second-in-time :max-cardinality 1 )
   (hour-of :type hour-in-time :max-cardinality 1 )
   (day-of :type day-in-time :max-cardinality 1)
   (month-of :type month-in-time :max-cardinality 1)
   (year-of :type year-in-time :max-cardinality 1 ))
  :constraint  (and (not (and (month-of ?x 2)
                             (> (the ?day (day-of ?x ?day))
                                29)))
                    (not (and (member-of ?x (4 6 9 11))
                              (> (the ?day (day-of ?x ?day))
                                30)))))

(def-class TIME-POINT (time-entity)
  "A point in time")

(def-class CALENDAR-DATE (time-point)
 "A calendar date is a time point in which month, day and year have 
  been specified"
  ((day-of :type day-in-time :cardinality 1)
   (month-of :type month-in-time :cardinality 1)
   (year-of :type year-in-time :cardinality 1)))



(def-class TIME-INTERVAL (time-entity)
  "An interval of time - e.g., 6 hours, 5 days, or '6 hours and 5 minutes'.  
   We use the same structure as a time point to express intervals")



(def-class TEMPORAL-THING (thing)
  "Like in Cyc, this is something which has a temporal extent."
  ((has-duration :type time-interval)
   (has-start-time :type time-point)
   (has-end-time :type time-point)))


(def-axiom DURATION-IS-START-TIME-MINUS-END-TIME
  "This axiom states the relation between duration, start time 
   and end time in a temporal thing"
  (=> (temporal-thing ?x)
      (= (the ?duration (has-duration ?x ?duration))
         (time-difference (the ?et (has-end-time ?x ?et))
                          (the ?st (has-start-time ?x ?st))))))

(def-function TIME-DIFFERENCE (?te1 ?te2) -> ?ti
  "The interval between two time entities."
  :def (and (time-entity ?te1)
            (time-entity ?te2)
            (time-interval ?ti)))