;;; -*- Mode: LISP; Syntax: Common-lisp; Base: 10; Package: OCML;   -*-

(in-package "OCML")

(in-ontology akt-support-ontology)

(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))
  
  :prove-by (or (and (variable-bound ?sub)
                      (member ?c (all-superclasses ?sub)))
                 (and (variable-bound ?c)
                      (member ?sub (all-subclasses ?c)))
                 (and 
                      (not (variable-bound ?c))
                      (not (variable-bound ?sub))
                      (class ?sub1)(class ?super1)
                      (subclass-of ?sub1 ?super1)))

  :iff-def (and (class ?sub) (class ?c)
                (forall ?inst
                        (=> (instance-of ?inst ?sub)
                            (instance-of ?inst ?c))))
  :no-proofs-by (:iff-def))

(def-function ALL-SUPERCLASSES (?class) -> ?supers
  :constraint (class ?class)
  :def (forall ?super (<=> (member ?super ?supers)
                           (subclass-of ?class ?super)))
  :lisp-fun  #'(lambda (class)
                 (let ((class-s (get-ocml-class class)))
                   (if class-s
                     (mapcar #'name (domain-superclasses class-s))))))

(def-function ALL-SUBCLASSES (?class) -> ?subs
  :constraint (class ?class)
   :def (forall ?sub (<=> (member ?sub ?subs)
                           (subclass-of ?sub ?class)))
   :lisp-fun  #'(lambda (class)
                  (let ((class-s (get-ocml-class class)))
                   (if class-s
                     (mapcar #'name (current-subclasses class-s))))))