;;; -*-Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; Extensions to frame ontology to support sugar-coated names
;;; for various slot constraints.  Inspired by the KL-ONE systems.

(in-package "ONTOLINGUA-USER")

(define-theory slot-constraint-sugar (frame-ontology)
  "Defines second-order relations for describing slot constraints
in a KL-ONE style.  Ontolingua recognizes these things and transforms
them into frame ontology terminology.  This ontology was formerly called
the kl-one-ontology.")

(in-theory 'slot-constraint-sugar)

(define-relation HAS-VALUES (?instance ?binary-relation ?set-of-values)
  "HAS-VALUES is a way to state the values of a slot on an instance.
Its third arguyment is a set, so that one can specify several
values at once.  For example, (HAS-VALUES i R (setof v_1 v_2 v_3)) means that
slot R applied to domain instance i maps to values v_1, v_2, and v_3.
In other words, R(i,v_1), R(i,v_2), and R(i,v_3) hold.
   There is no closed-world assumption implied; there may be
other values for the specified slot on a given domain instance."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (instance-of ?set-of-values set)
                (forall ?instance
                   (<=> (member ?value ?set-of-values)
                        (has-value ?instance ?binary-relation ?value)))))

;;; Moved HAS-VALUE to the frame ontology.

;(define-relation HAS-VALUE (?instance ?binary-relation ?slot-value)
;  "That is, a relation R HAS-VALUE v on domain instance i when R(i,v) holds.
;HAS-VALUE is a way to assert that a slot has a value on a domain instance.
;When used in a definition of a class, and the domain-instance argument is 
;the instance-variable defined for the class, the (HAS-VALUE ?i S v) means
;that slot S has the value v on all instances ?i of the class.
;   There is no closed-world assumption implied; in other words, there many be
;other values for the specified slot on a given domain instance."

;  :iff-def (and (instance-of ?binary-relation binary-relation)
;                (holds ?binary-relation ?instance ?slot-value))

;  :issues ("This is for completeness.  In definitions, one could 
;            say (slot ?instance value) instead of
;            (has-value ?instance slot value)."))


(define-relation HAVE-SAME-VALUES (?instance ?slot1 ?slot2)
  "Two binary relations R1 and R2 HAVE-SAME-VALUES if whenever
R1(i,v) holds for some value v, then R2(i,v) holds for the same
domain instance and value."

  :axiom-def (alias have-same-values same-values))


(define-relation HAS-AT-LEAST (?instance ?binary-relation ?n)
  "A binary relation HAS-AT-LEAST n values on domain instance i if there 
exist at least n distinct values v_j such that R(i,v_j) holds.
  When used in the definition of a class where ?i is the instance
variable, (HAS-AT-LEAST ?i R n) means that the slot R must have at
least n values on all instances of the class."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (instance-of ?n natural)
                (>= (value-cardinality ?instance ?binary-relation) ?n))

  :issues ((:see-also minimum-slot-cardinality value-cardinality)))


(define-relation HAS-AT-MOST (?instance ?binary-relation ?n)
  "A binary relation HAS-AT-LEAST n values on domain instance i if there 
exist no more than n distinct values v_j such that R(i,v_j) holds.
  When used in the definition of a class where ?i is the instance
variable, (HAS-AT-MOST ?i R n) means that the slot R can have at
most n values on any instances of the class."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (instance-of ?n natural)
                (=< (value-cardinality ?instance ?binary-relation) ?n))

  :issues ((:see-also maximum-slot-cardinality value-cardinality)))


(define-relation HAS-ONE (?instance ?binary-relation)
  "Binary relation R HAS-ONE value on domain instance i if there
exists exactly one value v such that R(i,v) holds.
  When used in the definition of a class where ?i is the instance
variable, (HAS-ONE ?i R)  means that the slot R must always have a
value, and only one value, when applied to instance of that class."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (= (value-cardinality ?instance ?binary-relation) 1)))

(define-relation HAS-SOME (?instance ?binary-relation)
  "Binary relation R HAS-SOME values on domain instance i if there
exists at least one value v such that R(i,v) holds.
  When used in the definition of a class where ?i is the instance
variable, (HAS-SOME ?i R)  means that the slot R must always have a
value when applied to instance of that class."

  :iff-def (has-at-least ?instance ?binary-relation 1))


(define-relation CAN-HAVE-ONE (?instance ?binary-relation)
  "A domain instance i CAN-HAVE-ONE value for a slot R if there
is at most 1 value v for which R(i,v) holds.
  Asserting (CAN-HAVE-ONE ?i R) in the definition of some class C,
where ?i is the instance variable for that class, is another way
of specifying that C is a domain restriction of R and R is 
a single-valued slot on C."

  :iff-def (has-at-most ?instance ?binary-relation 1)

  :issues ((:see-also HAS-AT-MOST SINGLE-VALUED-SLOT DOMAIN)))


(define-relation CANNOT-HAVE (?instance ?binary-relation)
  "A domain instance i CANNOT-HAVE a value for a slot R if 
it is inconsistent for R(i,v) to hold for any value v.
   CANNOT-HAVE is one way to restrict the domain of a relation
with respect to a class."

  :iff-def (not (instance-of ?instance (exact-domain ?binary-relation))))


(define-relation HAS-VALUE-OF-TYPE (?instance ?binary-relation ?type)
  "A binary relation R HAS-VALUE-OF-TYPE T on domain instance d
if there exists a v such that R(d,v) and v is an instance of T."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (instance-of ?type class)
                (>= (value-cardinality ?instance ?binary-relation) 1)
                (value-type ?instance ?binary-relation ?type))

  :issues ((:see-also HAS-SLOT-VALUE-OF-TYPE)))


(define-relation HAS-ONE-OF-TYPE (?instance ?binary-relation ?type)
  "A relation R HAS-ONE-OF-TYPE T on domain instance d
if there exists exactly one t such that R(c,t) and t is an instance of T."

  :iff-def (and (instance-of ?binary-relation binary-relation)
                (instance-of ?type class)
                (= (value-cardinality ?instance ?binary-relation) 1)
                (value-type ?instance ?binary-relation ?type))

  :issues ((:see-also HAS-SINGLE-SLOT-VALUE-OF-TYPE)))

(define-relation HAS-SLOT-VALUE (?class ?binary-relation ?slot-value)
  "A class C HAS-SLOT-VALUE v of relation R if for every instance i 
of C, R(i,v)."

  :iff-def (and (instance-of ?class class)
                (instance-of ?binary-relation binary-relation)
                (=> (instance-of ?instance ?class)
                    (holds ?binary-relation ?instance ?slot-value)))

  :issues ((:see-also
             "HAS-SLOT-VALUE corresponds to LOOM's ``FILLED-BY'' 
              and CLASSIC's ``FILLS''.")))


(define-relation HAS-SLOT-VALUE-OF-TYPE (?domain-class ?relation ?type)
  "A relation R HAS-SLOT-VALUE-OF-TYPE T with respect to domain class C
if for every instance i of C there exists a value v such that R(i,v) and v
is an instance of the class T."

  :iff-def (and (instance-of ?domain-class class)
                (instance-of ?relation binary-relation)
                (instance-of ?type class)
                (=> (instance-of ?instance ?domain-class)
                    (has-value-of-type ?instance ?relation ?type))))


(define-relation HAS-SINGLE-SLOT-VALUE-OF-TYPE (?class ?binary-relation ?type)
  "A relation R HAS-SINGLE-SLOT-VALUE-OF-TYPE T with respect to domain
class C if for every instance i of C there exists exactly one v such
that R(i,v) and v is an instance of T."

  :iff-def (and (instance-of ?class class)
                (instance-of ?binary-relation binary-relation)
                (instance-of ?type class)
                (single-valued-slot ?class ?binary-relation)
                (has-slot-value-of-type ?class ?binary-relation ?type))

  :issues ((:see-also
            "HAS-SINGLE-SLOT-VALUE-OF-TYPE is inspired by LOOM's ``THE'' operator.")))


(define-relation HAVE-SAME-SLOT-VALUES (?class ?slot1 ?slot2)
  "Let class C be in the domain of two binary relations R_1 and R_2.
The relation (have-same-values C R_1 R_2) means that the values of the
two relations are the same when applied to instances of the class."
  :axiom-def (alias have-same-slot-values same-slot-values))


(define-relation CAN-BE-ONE-OF (?instance ?set-of-classes)
  "An instance i CAN-BE-ONE-OF a set of classes S iff i is an instance
of at most one of the classes.  Inside the definition of a class,
the form (CAN-BE-ONE-OF ?i (setof C1 C2 ...)) is a convention for
stating (subclass-partition class (setof C1 C2 ...)).
The two forms are equivalent if each class C1, C2, ... is also defined to be
a subclass of C."

  :iff-def (and (forall ?class
                   (=> (member ?class ?set-of-classes)
                       (class ?class)))
                (forall ?class
                   (=> (member ?class ?set-of-classes)
                       (instance-of ?instance ?class)
                       (forall ?other-class
                          (=> (member ?other-class ?set-of-classes)
                              (not (= ?other-class ?class))
                              (not (instance-of ?instance ?other-class))))))))


(define-relation MUST-BE-ONE-OF (?instance ?set-of-classes)
  "An instance i MUST-BE-ONE-OF a set of classes S iff i is an instance
of at exactly one of the classes.  Inside the definition of a class,
the form (MUST-BE-ONE-OF ?i (setof C1 C2 ...)) is a convention for
stating (exhaustive-subclass-partition C (setof C1 C2 ...)).
The two forms are equivalent if each class C1, C2, ... is also defined to be
a subclass of C."

  :iff-def (and (can-be-one-of ?instance ?set-of-classes)
                (exists ?class
                   (and (member ?class ?set-of-classes)
                        (instance-of ?instance ?class)))))


(define-function COMPOSE* (@binary-relations) :-> ?composed-relation
  "Alias of COMPOSE, kept around for compatability."
  :axiom-def (alias compose* compose))

(define-relation VALUE-CLASS (?instance ?binary-relation ?type)
  :axiom-def (alias value-class value-type))