AKT Support Ontology v1.0 (OCML)

1 LOAD

 
 
;;; Mode: Lisp; Package: ocml
 
;;; The Open University
 
(in-package "OCML")
 
 

1.1 ontology AKT-SUPPORT-ONTOLOGY

 
(def-ontology akt-support-ontology
 
   :author "enrico"
 
   :allowed-editors ("john")
 
   :do-not-include-base-ontology? t
 
   :files ( "foundations" "basic" 
  "frames" "time" "new"))

2 FOUNDATIONS

 
 
;;; Mode: Lisp; Package: ocml
 
;;; The Open University
 
(in-package "OCML")
 
(in-ontology akt-support-ontology)
 
;;;A very simple top-level. We define something called THING, which
;;;is the top-level concept in the ontology. 
  We then distinguish two basic
;;;types of 'things': TANGIBLE-THING, something that has some physicality,
;;;and INTANGIBLE-THING, something which has not. We use a very open definition
;;;of being tangible: obviusly a physical object is tangible, but 
also a sub-atomic
;;;particle is tangible, even if some of them are very tricky (you do 
not see them)
;;;you only see the trace they leave behind. 
  Also a piece of software will be
;;;considered a tangible thing, it is something that you can see on a 
floppy disk.
;;;In contrast an algorithm will be an intangible, although the file 
that contains
;;;its implementation will be a tangible thing.
 
;;;This is a stop-gap top level. Over the course of teh project we 
may want to extend this
;;;and link to existing top levels (SUO, HPKB, CYC, Sowa, Guarino, etc.)
 
 

2.1 class THING

 
(def-class THING ()
 
   "This is the top-level concept in the AKT reference ontology"
 
   )
 
 

2.2 class INTANGIBLE-THING

 
(def-class INTANGIBLE-THING (thing)
 
   "This comes from HPKB upper level.
 
    The collection of things that are not physical -- are not made
 
    of, or encoded in, matter. Every Collection is an Intangible (even if its
 
    instances are tangible), and so are some Individuals.
 
    Caution: do not confuse `tangibility' with `perceivability' -- 
humans can perceive
 
    light even though it's intangible--at least in a sense.")
 

2.3 class TANGIBLE-THING

 
(def-class TANGIBLE-THING (thing)
 
   "Something which is not intangible")
 

2.4 axiom TANGIBLE-AND-INTANGIBLE-THINGS-ARE-DISJOINT

 
(def-axiom TANGIBLE-AND-INTANGIBLE-THINGS-ARE-DISJOINT
 
   (subclass-partition thing (set-of Tangible-Thing 
  Intangible-thing)))
 

2.5 class QUANTITY

 
(def-class QUANTITY (Intangible-thing)
 
   ((has-unit-of-measure :type unit-of-measure)
 
    (has-magnitude :type number)))
 

2.6 class UNIT-OF-MEASURE

 
(def-class UNIT-OF-MEASURE (Intangible-thing)
 
   "Any kind of unit of measure, metre, dollar, kilogram, etc..")
 
 

3 BASIC

 
 
;;; Mode: Lisp; Package: ocml
 
;;; The Open University
 
(in-package "OCML")
 
(in-ontology akt-support-ontology)
 
;;;Here we introduce a number of definitions, which provide
;;;the basic representational layer to define entities in the ontology.
;;;Here we include basic data types, such
;;;as strings, lists, sets and numbers, as well as basic logical concepts, such
;;;as FUNCTION and RELATION. 
  It also provides equality constructs 
and a meta-level
;;;relation HOLDS, which takes a rel, say ?rel, and a number of args, say ?args
;;;and it is satisfied iff ?rel is satisfied by ?args.
;;;The advantage of expliciting including here the representational layer
;;;for the set of AKT ontologies is that these become completely 
self-contained:
;;;all the notions required to specify any concept in the ontology 
are themselves
;;;to be found in the ontologies
 
;;;BASIC UNIFICATION MECHANISMS
 
 
;;;RELATION =

3.1 relation =

 
(def-relation = (?x ?y)
 
    "True if ?x and ?y do unify"
 
    :lisp-fun #'(lambda ( x y env)
 
                  (Let ((result (unify x y env)))
 
                    (if (eq result :fail)
 
                        :fail
 
                        (List result)))))
 
;;;RELATION ==

3.2 relation ==

 
(def-relation == (?x ?y)
 
    "True if ?x and ?y do unify and they also have the same structure.
 
     This means that either they are both atoms, or they are lists with
 
     the same structure"
 
    :lisp-fun #'(lambda ( x y env)
 
                  (Let ((result (unify-strong x y env)))
 
                    (if (eq result :fail)
 
                        :fail
 
                 
        (List result)))))
 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 

3.3 class LIST

 
(def-class LIST (Intangible-Thing) ?x
 
    "A 
  class representing lists."
 
    :iff-def (or (= ?x nil)
 
                 (= ?x (?a . ?b))))
 
 

3.4 instance NIL

 
(def-instance NIL list
 
   "The empty list")
 

3.5 relation NULL

 
(def-relation NULL (?l)
 
    "True if ?l is the empty list"
 
    :iff-def (= ?l nil))
 

3.6 function FIRST

 
(def-function FIRST (?l)
 
    "Takes the first element of a list. 
  If the list is empty
 
     the function returns :nothing"
 
   :constraint (list ?l)
 
   :body (if (== ?l (?a . ?b))
 
             ?a
 
             :nothing))
 

3.7 function REST

 
(def-function REST (?l)
 
    "Takes a list as argument, say ?l, removes the first element of ?s
 
     and returns the resulting list. 
  If ?l = nil, then :nothing is returned"
 
   :constraint (list ?l)
 
   :body (if (== ?l (?a . ?b))
 
             ?b
 
             :nothing))
 

3.8 function LIST-OF

 
(def-function LIST-OF (&rest ?els)
 
    "This is the primitive list constructor. 
  It is implemented in terms of
 
     the underlying LISP list construction primitive, LIST"
 
    :lisp-fun #'(lambda (&rest els)
 
                  (apply #'list els)))
 

3.9 function APPEND

 
(def-function APPEND (?l1 &rest ?ls)
 
   "Appends together a number of lists. I cannot be bothered giving 
its operational
 
    spec...so you only get a lisp attachment"
 
   :constraint (and (list ?l1)(every 
  ?ls list))
 
    :lisp-fun #'append)
 
 

3.10 function CONS

 
(def-function CONS (?el ?l)
 
   "Adds ?el to the beginning of list ?l.
 
    Note that this cons is less generic than the lisp function with 
the same name.
 
    Here the 2nd argument must be a list (in lisp, it can also be an atom)."
 
   :constraint (list ?l)
 
   :body (append (list-of ?el)
 
                 ?l))
 
 

3.11 function LENGTH

 
(def-function LENGTH (?l)
 
   "Computes the number of elements in a list"
 
   :constraint (list ?l)
 
   :body (if (= ?l nil)
 
           0
 
           (if (== ?l (?first . ?rest))
 
             (+ 1
 
                (length ?rest)))))
 

3.12 function REMOVE1

 
(def-function REMOVE1 (?el ?l)
 
   "Removes the first occurrence of ?el in ?l and returns the resulting list.
 
    If ?el is not a member of ?l then the result is ?l"
 
   :constraint (list ?l)
 
   :body (if (= ?l nil)
 
           ?l
 
           (if (== ?l (?el . ?rest))
 
             ?rest
 
             (if (== ?l (?first . ?rest))
 
               (cons ?first
 
                     (remove1 ?el ?rest))))))
 

3.13 function REMOVE

 
(def-function REMOVE (?el ?l)
 
   "Removes all occurrences of ?el in ?l and returns the resulting list.
 
    If ?el is not a member of ?l then the result is ?l"
 
   :constraint (list ?l)
 
   :body (if (= ?l nil)
 
           ?l
 
           (if (== ?l (?el . ?rest))
 
             (remove ?el ?rest)
 
             (if (== ?l (?first . ?rest))
 
               (cons ?first
 
                     (remove ?el ?rest))))))
 
 
 
 

3.14 relation MEMBER

 
(def-relation MEMBER (?el ?list)
 
   "A relation to check whether something is a member of a list"
 
   :constraint (list ?list)
 
   :iff-def (or (== ?list (?el . ?rest))
 
                (and (== ?list (?first . ?rest))
 
                     (member ?el ?rest))))
 

3.15 relation EVERY

 
(def-relation EVERY (?l ?rel)
 
   "True if for each term in ?l, say ?term, (holds ?rel ?term) is true.
 
    For instance, (every '(1 2 3) 'number) is satisfied, while
 
    (every '(1 2 pippo) 'number) is not"
 
   :constraint (unary-relation ?rel)
 
   :iff-def (or (= ?l nil)
 
                (and (== ?l (?first . ?rest))
 
                     (holds ?rel ?first)
 
                     (every ?rest ?rel))))
 
;;;FUNCTION BUTLAST

3.16 function BUTLAST

 
(def-function BUTLAST (?list)
 
    "Returns all the element of ?list, except the last one.
 
     If ?list = NIL, then :nothing is returned. 
  If ?list has
 
     length 1, then nil is returned"
 
    :constraint (list ?l)
 
    :body (cond ((null ?list) :nothing)
 
                ((null (rest ?list)) nil)
 
                ((true)
 
                 (cons (first ?list) (butlast (rest ?list))))))
 
 
;;;FUNCTION LAST

3.17 function LAST

 
(def-function LAST (?list)
 
    "Returns the last element of a list. 
  If ?list is empty
 
     then :nothing is returned"
 
   :constraint (list ?list)
 
   :body (cond ((null ?list) :nothing)
 
               ((null (rest ?list)) (first ?list))
 
               ((true) (last (rest ?list)))))
 
 
;;;;;;;;;;;;;;;;;;;;;;;;
 
 
;;;SET

3.18 class SET

 
(def-class SET (Intangible-Thing)
 
   "A set is something which is not an individual. In cyc sets are distinguished
 
    from collections. 
  Here we just use the term generically to refer to
 
    something which denotes a collection of elements, whether abstract or
 
    concrete.
 
    Functions and relations represent sets. ")
 

3.19 axiom BASIC-SET-TYPES-ARE-DISJOINT

 
(def-axiom BASIC-SET-TYPES-ARE-DISJOINT
 
   "There are three basic types of sets in our ontology, functions
 
    relations and enumerated sets and these do not intersect"
 
   (subclass-partition set (set-of function relation enumerated-set)))
 
 

3.20 function SET-OF

 
(def-function SET-OF (&rest ?args)
 
   "This is the basic set constructor to create a set by enumerating 
its elements.
 
    For instance, (setof 1 2) denotes the set {1 2}.
 
    We represent such a set as a list whose first item is :set"
 
   :body (cons :set ?args))
 
 

3.21 class ENUMERATED-SET

 
(def-class ENUMERATED-SET (set) ?x
 
   "A set represented as (:set-of el1 el_2...el_n), where no el_i is repeated"
 
   :constraint (list ?x)
 
   :iff-def (and (= ?x (:set . ?elements))
 
                 (not (exists ?el
 
                              (and (member ?el ?elements)
 
                                   (member ?el (remove1 ?el ?elements)))))))
 
 
 

3.22 class INDIVIDUAL

 
(def-class INDIVIDUAL (Thing) ?x
 
   "Something which is not a set. 
  For instance an instance of a class."
 
   :iff-def (not (set ?x))
 
 
   ;;;the definitions below are effective ways to prove whether
 
   ;;;somebody is an individual in OCML
 
   :prove-by (or
 
              (and (variable-bound ?x)
 
                   (not (set ?x)))
 
              (= ?x nil))
 
   :no-proofs-by (:iff-def)) ;;;:iff-def above is not a good way to 
prove things!
 
 
 

3.23 relation ELEMENT-OF

 
(def-relation ELEMENT-OF (?el ?set)
 
   "A relation to check whether something is an element of a set.
 
    Note that because functions and relations are sets, we can prove
 
    whether a tuple satisfies a relation or a function using ELEMENT-OF.
 
    For instance, (element-of '(1 2 3) '+) is satisfied because
 
    1+2=3 - see definitions below for an operationalization of this approach")
 

3.24 rule ELEMENT-OF-ENUMERATED-SET

 
(def-rule element-of-enumerated-set
 
   "An operationalization of element-of, which works with sets 
represented as lists."
 
   ((element-of ?el ?l) if
 
    (enumerated-set ?l)
 
    (member ?el (rest ?l))))
 

3.25 rule ELEMENT-OF-SET-AS-RELATION

 
(def-rule element-of-set-as-relation
 
   "A tuple, say  
 is an element of relation r iff
 
    (holds r ti t2 t3) is satisfied"
 
   ((element-of ?tuple ?rel) if
 
    (relation ?rel)
 
    (List ?tuple)
 
    (sentence-holds (cons ?rel ?tuple))))
 

3.26 rule ELEMENT-OF-SET-AS-FUNCTION

 
(def-rule element-of-set-as-function
 
   "A tuple, say  
 is an element of function f iff
 
    (= (apply f ti t2) t3) is satisfied"
 
   ((element-of ?el ?fun) if
 
    (function ?fun)
 
    (list ?el)
 
    (= (last ?el) (apply ?fun (butlast ?el)))))
 
 
 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
;;;NUMBER

3.27 class NUMBER

 
(def-class NUMBER (individual Intangible-thing)
 
   "The class of all numbers"
 
   :lisp-fun 
  #'(lambda (x env)
 
                  (let ((y (unbound-variable? x env)))
 
                    (if y ;;if y is unbound we return a 'sample' number
 
                      (list (cons (cons y 0) env))
 
                      (if (numberp (instantiate x env)) ;;;make sure 
to instantiate x
 
                        (list env)
 
                        :fail)))))
 
 
;;; RELATION <

3.28 relation <

 
(def-relation < (?x ?y)
 
    "A predicate to test whether a number is less than another"
 
    :constraint (and (number ?x)(number ?y))
 
    :lisp-fun #'(lambda (x y env)
 
                  (if (< (instantiate x env)
 
                         (instantiate y env))
                
     (List env)
                
     :fail)))
;;;RELATION >

3.29 relation >

 
(def-relation > (?x ?y)
 
    "A predicate to test whether a number is greater than another"
 
    :constraint (and (number ?x)(number ?y))
 
    :lisp-fun #'(lambda (x y env)
 
                  (if (> (instantiate x env)
 
                         (instantiate y env))
                
     (List env)
                
     :fail)))
 
 

3.30 class POSITIVE-NUMBER

 
(def-class POSITIVE-NUMBER (number) ?x
 
   :iff-def (and (number ?x)
 
                 (> ?x 0)))
 

3.31 class NEGATIVE-NUMBER

 
(def-class NEGATIVE-NUMBER (number) ?x
 
   
 :iff-def (and (number ?x)
 
                 (< ?x 0)))
 

3.32 class NON-NEGATIVE-NUMBER

 
(def-class NON-NEGATIVE-NUMBER (number) ?x
 
    :iff-def (and (number ?x)
 
                  (not (negative-number ?x))))
 
 

3.33 axiom POS-NEG-NUMBERS-EXHAUSTIVE-PARTITION

 
(def-axiom POS-NEG-NUMBERS-EXHAUSTIVE-PARTITION
 
   (exhaustive-subclass-partition number (set-of positive-number 
negative-number)))
 
 
 
 

3.34 class INTEGER

 
(def-class INTEGER (number)
 
    "The class of all integers"
 
    :lisp-fun 
  #'(lambda (x env)
 
                  (let ((y (unbound-variable? x env)))
 
                    (if y ;;if y is unbound we return a 'sample' integer
 
                      (list (cons (cons y 0) env))
 
                      (if (integerp (instantiate x env)) ;;;make sure 
to instantiate x
 
                        (list env)
 
                        :fail)))))
 
 

3.35 class POSITIVE-INTEGER

 
(def-class POSITIVE-INTEGER (integer) ?x
 
   :iff-def (and (integer ?x)
 
                 (> ?x 0)))
 

3.36 class NEGATIVE-INTEGER

 
(def-class NEGATIVE-INTEGER (integer) ?x
 
   :iff-def (and (integer ?x)
 
                 (< ?x 0)))
 

3.37 class NON-NEGATIVE-INTEGER

 
(def-class NON-NEGATIVE-INTEGER (integer) ?x
 
   :iff-def (and (integer ?x)
 
                 (not (negative-integer ?x))))
 
 

3.38 function +

 
(def-function + (?X &rest ?y)
 
   "Adds numbers"
 
   :constraint (and (number ?x) (number ?y))
 
   :lisp-fun #'+)
 

3.39 function *

 
(def-function * (?X ?y)
 
   "Multiplies numbers"
 
   :constraint (and (number ?x) (number ?y))
 
    :lisp-fun #'*)
 

3.40 function SQUARE

 
(def-function SQUARE (?X)
 
   :constraint 
  (number ?x)
 
   :body (* ?X ?X))
 

3.41 function -

 
(def-function - (?X &rest ?y)
 
   "Subtracts numbers"
 
   :constraint (and (number ?x) (number ?y))
 
   :lisp-fun #'(lambda (x &rest y)
 
                 (apply #'- x y)))
 

3.42 function /

 
(def-function / (?X ?y)
 
   "Divides numbers"
 
   :constraint (and (number ?x) (number ?y))
 
   :lisp-fun #'/)
 
;;;;;;;;;;;;;;;;;;;;;
 

3.43 class STRING

 
(def-class STRING (individual intangible-thing)
 
    "A primitive class representing strings"
 
    :lisp-fun 
  #'(lambda (x env)
 
                   (let ((y (unbound-variable? x env)))
 
                    (if y
 
                      (list (cons (cons y "SAMPLE-STRING") env))
 
                      (if (stringp (instantiate x env))
 
                        (list env)
 
                        :fail)))))
 
;;;;;;;;;;;;;;;;;;;;;
 

3.44 class RELATION

 
(def-class RELATION (set)
 
   "The class of defined relations. 
  We assume fixed arity"
 
   :lisp-fun #'(lambda (x env)
 
                  (let ((y (unbound-variable? x env)))
 
                    (if y
 
                      (mapcar #'(lambda (rel)
 
                    
                 (cons (cons y rel) env))
 
                              (all-relations))
 
                      (if (get-relation (instantiate x env)) ;;;make 
sure to instantiate x
 
                        (list env)
 
                        :fail)))))
 
 

3.45 class UNARY-RELATION

 
(def-class UNARY-RELATION (relation) ?r
 
   :iff-def (and (relation ?r)
 
                 (= (arity ?r) 1)))
 
 

3.46 class BINARY-RELATION

 
(def-class BINARY-RELATION (relation) ?r
 
   :iff-def (and (relation ?r)
 
                 (= (arity ?r) 2)))
 

3.47 relation TRUE

 
(def-relation TRUE ()
 
   "This is always satisfied"
 
    :lisp-fun #'(lambda (env) (list env)))
 

3.48 relation FALSE

 
(def-relation FALSE ()
 
   "This is never satisfied"
 
    :lisp-fun #'(lambda (env) :fail))
 
 

3.49 function ARITY

 
(def-function ARITY (?x)
 
   "The arity of a function or relation. 
  If a function or relation
 
    has variable arity, then we treat the last argument as if it were
 
    a sequence variable. 
  For instance the argument list for + is
 
    (?x &rest ?y). 
  In this case we say that + has arity 2.
 
    It is important to note that OCML does not support relations with variable
 
    arity. 
  The only exception is HOLDS, which has variable arity and 
is built in
 
    the OCML proof system"
 
 
   :constraint (or (function ?X)(relation ?X))
 
   :body 
  (in-environment
 
           ((?l . (the-schema ?x))
 
            (?n . (length ?l)))
 
           (if (every ?l variable)
 
             ?n
 
             ;we assume that the only non-var can be &rest
 
             (- ?n 1))))
 

3.50 relation VARIABLE

 
(def-relation VARIABLE (?x)
 
   "True of an OCML variable"
 
   :lisp-fun #'(lambda (x env)
 
             
     (if
 
                   (variable? (instantiate x env))
 
                   (list env)
 
                   :fail)))
 

3.51 relation VARIABLE-BOUND

 
(def-relation VARIABLE-BOUND (?var)
 
   "True if ?var is 
  bound in teh current environment"
 
   :lisp-fun #'(lambda (x env)
 
     
             (if
 
                   (unbound-variable? x env)
 
                   :fail
 
                   (list env))))
 

3.52 function THE-SCHEMA

 
(def-function THE-SCHEMA (?x)
 
   "The schema of a function or relation"
 
   :constraint (or (function ?X)(relation ?X))
 
   :body (if (relation ?x)
 
           (relation-schema ?x)
 
           (if (function ?x)
 
             (function-schema ?x)
 
             :nothing)))
 

3.53 function FUNCTION-SCHEMA

 
(def-function FUNCTION-SCHEMA (?f)
 
   :constraint (function ?f)
 
    :lisp-fun #'(lambda (x)
 
                   (rename-variables (schema (get-function x)))))
 

3.54 function RELATION-SCHEMA

 
(def-function RELATION-SCHEMA (?rel)
 
   :constraint (relation ?rel)
 
   :lisp-fun #'(lambda (x)
 
                  (rename-variables (schema (get-relation x)))))
 
 
 

3.55 relation HOLDS

 
(def-relation HOLDS (?rel &rest ?args)
 
   "A meta-level relation which is true iff the sentence (?rel . ?args) is true.
 
    The length of ?args must be consistent with the arity of the relation"
 
   :constraint (and (relation ?r)
 
                    (= (arity ?rel)
 
                       (length ?args))))
 

3.56 relation SENTENCE-HOLDS

 
(def-relation SENTENCE-HOLDS (?sentence)
 
   "The same as HOLDS, but takes only one argument, a sentence whose truth
 
    value is to be checked"
 
   :constraint (and (== ?sentence (?rel . ?args ))
 
                    (relation ?rel)
 
                    (= (arity ?rel)
 
                       (length ?args)))
 
   :lisp-fun #'(lambda (sent env)
 
                 (ask-top-level
 
                  (cons 'holds (instantiate sent env))
 
                  :env env
 
                  :all t)))
 
 
 

3.57 class FUNCTION

 
(def-class FUNCTION (set)
 
   "The class of all defined functions"
 
   :lisp-fun #'(lambda (x env)
 
                  (let ((y (unbound-variable? x env)))
 
                    (if y
 
                      (mapcar #'(lambda (rel)
 
    
                                 (cons (cons y rel) env))
 
                              (all-functions))
 
                      (if (ocml-function?
 
                           (instantiate x env))
 
                        (list env)
 
                        :fail)))))
 
 
 
 

3.58 function APPLY

 
(def-function APPLY (?f ?args)
 
   "(apply f (arg1 .....argn)) is the same as
 
    (f arg1 ....argn)"
 
   :constraint (and (function ?f)
 
                    (list ?args)))
 
 

4 FRAMES

 
 
;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; Package: OCML; 
   -*-
 
(in-package "OCML")
 
(in-ontology akt-support-ontology)
 
;;;here I have defined a few basic notions we need to have to talk 
about frame-based models
 

4.1 class CLASS

 
(def-class CLASS (unary-relation)
 
   "The class of all classes. 
  We consider a class as a unary 
relation, true for all its instances"
 
   :lisp-fun 
  #'(lambda (x env)
 
                (let ((y (unbound-variable? x env)))
 
                    (if y
 
                      (mapcar #'(lambda (rel)
 
                                  (cons (cons y rel) env))
 
                     
          (all-ocml-classes))
 
                      (if (get-ocml-class
 
                           (instantiate x env))
 
                        (list env)
 
                        :fail)))))
 

4.2 class CLASS-PARTITION

 
(def-class CLASS-PARTITION (enumerated-set) ?set-of-classes
 
   "A set of mutually disjoint classes. 
  Disjointness of
 
    classes is a special case of disjointness of sets."
 
   :constraint (enumerated-set ?set-of-classes)
 
   :iff-def (and (enumerated-set ?set-of-classes)
 
                 (forall ?C
 
                
          (=> (element-of ?C ?set-of-classes)
 
                             (class ?C)))
 
                 (forall (?C1 ?C2)
 
                         (=> (and (element-of ?C1 ?set-of-classes)
 
                                  (element-of ?C2 ?set-of-classes)
 
                                  (not (= ?C1 ?C2)))
 
                             (forall (?i)
 
                                     (=> (instance-of ?i ?C1)
 
                                         (not (instance-of ?i ?C2)))))))
 
   :avoid-infinite-loop t)
 
 

4.3 relation SUBCLASS-PARTITION

 
(def-relation SUBCLASS-PARTITION (?C ?class-partition)
 
    "A subclass-partition of a class C is a set of
 
     subclasses of C that are mutually disjoint."
 
    :iff-def (and (class ?C)
 
                  (class-partition ?class-partition)
 
                  (forall ?subclass
 
                          (=> (element-of ?subclass ?class-partition)
 
                              (subclass-of ?subclass ?C)))))
 

4.4 relation EXHAUSTIVE-SUBCLASS-PARTITION

 
(def-relation EXHAUSTIVE-SUBCLASS-PARTITION (?C ?class-partition)
 
    "A subrelation-partition of a class C is a set of
 
     mutually-disjoint classes (a subclass partition) which covers C.
 
     Every instance of C is is an instance of exactly one of the subclasses
 
     in the partition."
 
    :iff-def (and (subclass-partition ?C ?class-partition)
 
                  (forall ?instance
 
                          (=> (instance-of ?instance ?C)
 
                              (exists ?subclass
 
                                      (and (element-of ?subclass 
?class-partition)
 
                                           (instance-of ?instance 
?subclass)))))))
 

4.5 relation INSTANCE-OF

 
(def-relation INSTANCE-OF (?x ?c)
 
   "This definition relates the notion of 'being an instance' to the notion
 
    of satisfying a relation: ?I is an instance of a class ?c,
 
    iff (holds ?I ?c) is true"
 
    :constraint (class ?c)
 
    :iff-def (and (class ?c)
 
                  (holds ?c ?x)))
 

4.6 relation SUBCLASS-OF

 
(def-relation SUBCLASS-OF (?sub ?c)
 
   "?sub is a subclass of ?c if every instance of ?sub is also an instance of
 
    ?c. 
  Note that according to this definition every class is a 
subclass of itself"
 
 
   :constraint (and (class ?sub)(class ?c))
 
   :iff-def (and (class ?sub) (class ?c)
 
                 (forall ?inst
 
          
                (=> (instance-of ?inst ?sub)
 
                             (instance-of ?inst ?c)))))
 

5 TIME

 
 
;;; 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)
 

5.1 class YEAR-IN-TIME

 
(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)
 

5.2 class MONTH-IN-TIME

 
(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)
 

5.3 class DAY-IN-TIME

 
(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)
 

5.4 class HOUR-IN-TIME

 
(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)
 

5.5 class SECOND-IN-TIME

 
(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)
 

5.6 class MINUTE-IN-TIME

 
(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)
 
 

5.7 class TIME-ENTITY

 
(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)))))
 

5.8 class TIME-POINT

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

5.9 class CALENDAR-DATE

 
(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)))
 

5.10 class CALENDAR-DATE

 
(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)))
 
 

5.11 class TIME-INTERVAL

 
(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")
 
 
 

5.12 class TEMPORAL-THING

 
(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)))
 
 

5.13 axiom DURATION-IS-START-TIME-MINUS-END-TIME

 
(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))))))
 

5.14 function TIME-DIFFERENCE

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