;;(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-theoryJAT-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-classINTEGER-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-functionI-LOWER-BOUND(?range) :-> ?integer "(I-LOWER-BOUND r) denotes the integer lower bound of range r." :def (and (integer-range ?range) (integer ?integer))) (define-functionI-UPPER-BOUND(?range) :-> ?integer "(I-UPPER-BOUND r) denotes the integer upper bound of range r." :def (and (integer-range ?range) (integer ?integer))) (define-classREAL-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-functionR-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-functionR-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-classTIME-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-functionTIME-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-functionTIME-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-functionTIME-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-relationBEFORE(?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-relationAFTER(?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-relationMEETS(?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-relationEQUALS(?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-relationDURING(?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-relationOVERLAPS(?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-relationSTARTS(?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-relationFINISHES(?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-relationBEFORE=(?tr1 ?tr2) :iff-def (or (before ?tr1 ?tr2) (meets ?tr1 ?tr2)) ) (define-relationAFTER=(?tr1 ?tr2) :iff-def (or (after ?tr1 ?tr2) (meets ?tr2 ?tr1)) ) (define-relationDURING=(?tr1 ?tr2) :iff-def (or (during ?tr1 ?tr2) (starts ?tr1 ?tr2) (finishes ?tr1 ?tr2) (equals ?tr1 ?tr2)) ) (define-relationOVERLAPS=(?tr1 ?tr2) :iff-def (or (overlaps ?tr1 ?tr2) (meets ?tr1 ?tr2)) ) (define-relationSTART=(?tr1 ?tr2) :iff-def (or (starts ?tr1 ?tr2) (equals ?tr1 ?tr2)) ) (define-relationFINISHES=(?tr1 ?tr2) :iff-def (or (finishes ?tr1 ?tr2) (equals ?tr1 ?tr2)) ) (define-relationDISJOINT-TR(?tr1 ?tr2) "time ranges ?tr1 and ?tr2 do not overlap" :iff-def (or (before ?tr1 ?tr2) (before ?tr2 ?tr1)) ) (define-functionTR+(?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-classTIME-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-classYEAR-NUMBER(?year) "YEAR-NUMBER deontes a year of A.D." :def (integer ?year) ) (define-classMONTH-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-classMONTH-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-instancejanuary(month-name)) (define-instancefebruary(month-name)) (define-instancemarch(month-name)) (define-instanceapril(month-name)) (define-instancemay(month-name)) (define-instancejune(month-name)) (define-instancejuly(month-name)) (define-instanceaugust(month-name)) (define-instanceseptember(month-name)) (define-instanceoctober(month-name)) (define-instancenovember(month-name)) (define-instancedecember(month-name)) (define-classDAY-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-classDAY-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-instancesunday(day-name)) (define-instancemonday(day-name)) (define-instancetuesday(day-name)) (define-instancewednesday(day-name)) (define-instancethursday(day-name)) (define-instancefriday(day-name)) (define-instancesaturday(day-name)) (define-classHOUR-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-classMINUTE-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-classSECOND-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-functionTIME-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-functionTIME-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-functionTIME-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-functionTIME-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-functionTIME-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-functionTIME-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-functionTIME-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-functionTIME-POINT.SECOND(?time-point) :-> ?second "TIME-SECOND denotes a second of a time point." :def (and (time-point ?time-point) (second-number ?second)) ) (define-functionTIME-POINT.UNIT(?time-point) :-> ?unit "TIME-UNIT denotes a unit of a time point." :def (and (time-point ?time-point) (duration ?unit)) ) (define-relationTP=(?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-relationTP<(?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-relationTP>(?tp1 ?tp2) "inverse of TP<" :iff-def (tp< ?tp2 ?tp1) ) (define-functionTP+(?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-classDURATION(?duration) "DURATION denotes a period of time. It consists of a value and a measure" :def (individual ?duration) ) (define-functionDURATION.VALUE(?duration) :-> ?value "DURATION.VALUE returns a length of a duration in a cetain measure." :def (and (duration ?duration) (integer ?value)) ) (define-functionDURATION.MEASURE(?duration) :-> ?measure "DURATION.MEASURE returns a mesure of a length of a duration." :def (and (duration ?duration) (temporal-measure ?measure)) ) (define-relationDR=(?dr1 ?dr2) "Two duration is the same length." :def (and (duration ?dr1) (duration ?dr2)) ) (define-relationDR<(?dr1 ?dr2) "A duration ?dr1 is shorter than a duration ?dr2." :def (and (duration ?dr1) (duration ?dr2)) ) (define-relationDR>(?dr1 ?dr2) :iff-def (dr< ?dr2 ?dr1) ) (define-functionDR+(?dr1 ?dr2) :-> ?dr3 :def (and (duration ?dr1) (duration ?dr2) (duration ?dr3)) );;;; Definitions related to TEMPORAL-MEASURE;;(define-classTEMPORAL-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-instanceyear(temporal-measure)) (define-instancemonth(temporal-measure)) (define-instanceday(temporal-measure)) (define-instancehour(temporal-measure)) (define-instanceminute(temporal-measure)) (define-instancesecond(temporal-measure))