;;(C) Copyright IBM Corp. 1992
;; This file is included in the IBM Research Report RT0084,
;; "Task-Specific Language Constructs for Describing Constrints in
;; Job Assignment Probelms" by T.Hama, M.Hori, and Y.Nakamura.
;;
(in-package "ONTOLINGUA-USER")
(define-theory JAT-GENERIC (frame-ontology)
"This theory defines a generic ontology. Concepts in this ontolgy
can be shared in several different tasks. Only temporal concepts are
defined at present.
This theory is based on Ontolingua V 3.0")
(in-theory 'JAT-GENERIC)
;;
;; Definitions of second order classes
;;
(define-class INTEGER-RANGE (?class)
"An integer range is a class of integers specified by lower
and upper bounds. Instances of an integer-range are integers."
:iff-def (and (class ?class)
(subclass-of ?class integer)
(= (value-cardinality ?class I-LOWER-BOUND) 1)
(= (value-cardinality ?class I-UPPER-BOUND) 1)
(forall ?i (=> (instance-of ?i ?class)
(and (=< (i-lower-bound ?class) ?i)
(=< ?i (i-upper-bound ?class)))))))
(define-function I-LOWER-BOUND (?range) :-> ?integer
"(I-LOWER-BOUND r) denotes the integer lower bound of range r."
:def (and (integer-range ?range)
(integer ?integer)))
(define-function I-UPPER-BOUND (?range) :-> ?integer
"(I-UPPER-BOUND r) denotes the integer upper bound of range r."
:def (and (integer-range ?range)
(integer ?integer)))
(define-class REAL-RANGE (?class)
"An real range is a class of real numbers specified by lower
and upper bounds. Instances of an real-range are real numbers."
:iff-def (and (class ?class)
(subclass-of ?class real-number)
(= (value-cardinality ?class R-LOWER-BOUND) 1)
(= (value-cardinality ?class R-UPPER-BOUND) 1)
(forall ?i (=> (instance-of ?i ?class)
(and (=< (r-lower-bound ?class) ?i)
(=< ?i (r-upper-bound ?class)))))))
(define-function R-LOWER-BOUND (?range) :-> ?real
"(R-LOWER-BOUND r) denotes the real lower bound of range r."
:def (and (real-range ?range)
(real-number ?real)))
(define-function R-UPPER-BOUND (?range) :-> ?real
"(R-UPPER-BOUND r) denotes the real upper bound of range r."
:def (and (real-range ?range)
(real-number ?real)))
;;
;; Definitions related to TIME-RANGE
;;
(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 (tp= (tp+ (time-range.start-time ?time-range)
(time-range.duration ?time-range))
(time-range.end-time ?time-range))
)
(define-function TIME-RANGE.START-TIME (?time-range) :-> ?time-point
"(TR-START-TIME 'tr) denotes a start time of a time range tr."
:def (and (time-range ?time-range)
(time-point ?time-point))
)
(define-function TIME-RANGE.END-TIME (?time-range) :-> ?time-point
"(TR-END-TIME 'tr) denotes an end time of a time range tr."
:def (and (time-range ?time-range)
(time-point ?time-point))
)
(define-function TIME-RANGE.DURATION (?time-range) :-> ?duration
"(TR-END-DURATION 'tr) denotes a duration of a time range tr."
:def (and (time-range ?time-range)
(duration ?duration))
)
(define-relation BEFORE (?tr1 ?tr2)
"a time range ?tr1 preceeds a time ranage ?tr2."
:iff-def (tp< (time-range.end-time ?tr1)
(time-range.start-time ?tr2))
)
(define-relation AFTER (?tr1 ?tr2)
"a time range ?tr1 succeeds a time range ?tr2."
:iff-def (tp< (time-range.end-time ?tr2)
(time-range.start-time ?tr1))
:equivalent (before ?tr2 ?tr1) ;redundant
)
(define-relation MEETS (?tr1 ?tr2)
"a time range ?tr1 ends at the same time a time range ?tr2 starts."
:iff-def (tp= (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
)
(define-relation EQUALS (?tr1 ?tr2)
"a time range ?tr1 is identical to a time range ?tr2."
:iff-def (and (tp= (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(tp= (time-range.end-time ?tr1)
(time-range.end-time ?tr2)))
)
(define-relation DURING (?tr1 ?tr2)
"a time range ?tr1 is properly included in a time range ?tr2."
:iff-def (and (tp> (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(tp< (time-range.end-time ?tr1)
(time-range.end-time ?tr2)))
)
(define-relation OVERLAPS (?tr1 ?tr2)
"a time range ?tr1 and a time range ?tr2 overlaps."
:iff-def (and (tp< (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(tp< (time-range.start-time ?tr2)
(time-range.end-time ?tr1))
(tp< (time-range.end-time ?tr1)
(time-range.end-time ?tr2)))
)
(define-relation STARTS (?tr1 ?tr2)
"a time range ?tr1 and a time range ?tr2 starts at the same time
and a duration of ?tr1 is shorter than that of ?tr2."
:iff-def (and (tp= (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(tp< (time-range.end-time ?tr1)
(time-range.end-time ?tr2)))
)
(define-relation FINISHES (?tr1 ?tr2)
"a time range ?tr1 and a time range ?tr2 ends at the same time and
a duration of ?tr1 is shorter than that of ?tr2."
:iff-def (and (tp> (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(tp= (time-range.end-time ?tr1)
(time-range.end-time ?tr2)))
)
(define-relation BEFORE= (?tr1 ?tr2)
:iff-def (or (before ?tr1 ?tr2)
(meets ?tr1 ?tr2))
)
(define-relation AFTER= (?tr1 ?tr2)
:iff-def (or (after ?tr1 ?tr2)
(meets ?tr2 ?tr1))
)
(define-relation DURING= (?tr1 ?tr2)
:iff-def (or (during ?tr1 ?tr2)
(starts ?tr1 ?tr2)
(finishes ?tr1 ?tr2)
(equals ?tr1 ?tr2))
)
(define-relation OVERLAPS= (?tr1 ?tr2)
:iff-def (or (overlaps ?tr1 ?tr2)
(meets ?tr1 ?tr2))
)
(define-relation START= (?tr1 ?tr2)
:iff-def (or (starts ?tr1 ?tr2)
(equals ?tr1 ?tr2))
)
(define-relation FINISHES= (?tr1 ?tr2)
:iff-def (or (finishes ?tr1 ?tr2)
(equals ?tr1 ?tr2))
)
(define-relation DISJOINT-TR (?tr1 ?tr2)
"time ranges ?tr1 and ?tr2 do not overlap"
:iff-def (or (before ?tr1 ?tr2)
(before ?tr2 ?tr1))
)
(define-function TR+ (?tr1 ?duration) :-> ?tr2
"TR+ denotes a time range ?tr2 whose length is longer that ?tr1 by
a duration ?duration."
:iff-def (and (= (time-range.start-time ?tr1)
(time-range.start-time ?tr2))
(= (tp+ (time-range.end-time ?tr1) ?duration)
(time-range.end-time ?tr2)))
)
;;
;; Definition related to TIME-POINT
;;
(define-class TIME-POINT (?time-point)
"TIME denotes a cetain point of time. It consists of year, month,
day, hour, minute, second, and a unit of time. Any details smaller
than a unit of a time are not defined. For example, if a unit of time
is 2 hour, values of time-minute and time-second are meaningless."
:def (individual ?time-point)
)
(define-class YEAR-NUMBER (?year)
"YEAR-NUMBER deontes a year of A.D."
:def (integer ?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-class MONTH-NAME (?month)
"MONTH-NAME denotes a name of a month of a year."
:iff-def (member ?month
(setof january february march april may june july
august september october november december))
)
(define-instance january (month-name))
(define-instance february (month-name))
(define-instance march (month-name))
(define-instance april (month-name))
(define-instance may (month-name))
(define-instance june (month-name))
(define-instance july (month-name))
(define-instance august (month-name))
(define-instance september (month-name))
(define-instance october (month-name))
(define-instance november (month-name))
(define-instance december (month-name))
(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-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-instance sunday (day-name))
(define-instance monday (day-name))
(define-instance tuesday (day-name))
(define-instance wednesday (day-name))
(define-instance thursday (day-name))
(define-instance friday (day-name))
(define-instance saturday (day-name))
(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-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-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-function TIME-POINT.YEAR (?time-point) :-> ?year
"TIME-POINT.YEAR denotes a year of a time point."
:def (and (time-point ?time-point)
(year-number ?year))
)
(define-function TIME-POINT.MONTH (?time-point) :-> ?month
"TIME-POINT.MONTH denotes a month of a time point."
:def (and (time-point ?time-point)
(month-number ?month))
)
(define-function TIME-POINT.MONTH-NAME (?time-point) :-> ?month
"TIME-POINT.MONTH-NAME denotes a name of a month of a time point."
:def (and (time-point ?time-point)
(month-name ?month))
)
(define-function TIME-POINT.DAY (?time-point) :-> ?day
"TIME-POINT.DAY denotes a day of a time point."
:def (and (time-point ?time-point)
(day-number ?day))
)
(define-function TIME-POINT.DAY-NAME (?time-point) :-> ?day
"TIME-POINT.DAY-NAME denotes a name of a day of a time point."
:def (and (time-point ?time-point)
(day-name ?day))
)
(define-function TIME-POINT.HOUR (?time-point) :-> ?hour
"TIME-POINT.HOUR denotes an hour of a time point."
:def (and (time-point ?time-point)
(hour-number ?hour))
)
(define-function TIME-POINT.MINUTE (?time-point) :-> ?minute
"TIME-POINT.MINUTE denotes a minute of a time point."
:def (and (time-point ?time-point)
(minute-number ?minute))
)
(define-function TIME-POINT.SECOND (?time-point) :-> ?second
"TIME-SECOND denotes a second of a time point."
:def (and (time-point ?time-point)
(second-number ?second))
)
(define-function TIME-POINT.UNIT (?time-point) :-> ?unit
"TIME-UNIT denotes a unit of a time point."
:def (and (time-point ?time-point)
(duration ?unit))
)
(define-relation TP= (?tp1 ?tp2)
" a time point ?tp1 is equal to a time point ?tp2."
:iff-def (and (= (time-point.year ?tp1) (time-point.year ?tp2))
(= (time-point.month ?tp1) (time-point.month ?tp2))
(= (time-point.day ?tp1) (time-point.day ?tp2))
(= (time-point.hour ?tp1) (time-point.hour ?tp2))
(= (time-point.minute ?tp1) (time-point.minute ?tp2))
(= (time-point.second ?tp1) (time-point.second ?tp2)))
)
(define-relation TP< (?tp1 ?tp2)
"a time point ?tp1 preceeds a time point ?tp2."
:iff-def (or (< (time-point.year ?tp1)
(time-point.year ?tp2))
(and (= (time-point.year ?tp1)
(time-point.year ?tp2))
(or (< (time-point.month ?tp1)
(time-point.month ?tp2))
(and (= (time-point.month ?tp1)
(time-point.month ?tp2))
(or (< (time-point.day ?tp1)
(time-point.day ?tp2))
(and (= (time-point.day ?tp1)
(time-point.day ?tp2))
(or (< (time-point.hour ?tp1)
(time-point.hour ?tp2))
(and (= (time-point.hour ?tp1)
(time-point.hour ?tp2))
(or (< (time-point.minute ?tp1)
(time-point.minute ?tp2))
(and (= (time-point.minute ?tp1)
(time-point.minute ?tp2))
(or (< (time-point.second ?tp1)
(time-point.second ?tp2)))))))))))))
)
(define-relation TP> (?tp1 ?tp2)
"inverse of TP<"
:iff-def (tp< ?tp2 ?tp1)
)
(define-function TP+ (?tp1 ?duration) :-> ?tp2
"A difference between tow time points ?tp1 and ?tp2 is a
duration ?duration."
:def (and (time-point ?tp1)
(duration ?duration)
(time-point ?tp2))
)
;;
;; Definitions related to DURATION
;;
(define-class DURATION (?duration)
"DURATION denotes a period of time. It consists of a value and a
measure"
:def (individual ?duration)
)
(define-function DURATION.VALUE (?duration) :-> ?value
"DURATION.VALUE returns a length of a duration in a cetain measure."
:def (and (duration ?duration)
(integer ?value))
)
(define-function DURATION.MEASURE (?duration) :-> ?measure
"DURATION.MEASURE returns a mesure of a length of a duration."
:def (and (duration ?duration)
(temporal-measure ?measure))
)
(define-relation DR= (?dr1 ?dr2)
"Two duration is the same length."
:def (and (duration ?dr1)
(duration ?dr2))
)
(define-relation DR< (?dr1 ?dr2)
"A duration ?dr1 is shorter than a duration ?dr2."
:def (and (duration ?dr1)
(duration ?dr2))
)
(define-relation DR> (?dr1 ?dr2)
:iff-def (dr> ?dr2 ?dr1)
)
(define-function DR+ (?dr1 ?dr2) :-> ?dr3
:def (and (duration ?dr1)
(duration ?dr2)
(duration ?dr3))
)
;;
;; Definitions related to TEMPORAL-MEASURE
;;
(define-class TEMPORAL-MEASURE (?measure)
"TEMPORAL-MEASURE denotes a measure of a length of a temporal
interval."
:iff-def (member ?measure
(setof year month day hour minute second))
)
(define-instance year (temporal-measure))
(define-instance month (temporal-measure))
(define-instance day (temporal-measure))
(define-instance hour (temporal-measure))
(define-instance minute (temporal-measure))
(define-instance second (temporal-measure))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber