;;; -*-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 ?instance ?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) 
                (=< 0 (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 ?class ?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))