;;; -*-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-theoryslot-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-relationHAS-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-relationHAVE-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-relationHAS-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-relationHAS-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-relationHAS-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-relationHAS-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-relationCAN-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-relationCANNOT-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-relationHAS-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-relationHAS-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-relationHAS-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-relationHAS-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-relationHAS-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-relationHAVE-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-relationCAN-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-relationMUST-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-functionCOMPOSE*(@binary-relations) :-> ?composed-relation "Alias of COMPOSE, kept around for compatability." :axiom-def (alias compose* compose)) (define-relationVALUE-CLASS(?instance ?binary-relation ?type) :axiom-def (alias value-class value-type))