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.

**Last modified:***Friday, 2 April 1993***Source code: slot-constraint-sugar.lisp****List of other known theories**

Frame-OntologyKif-RelationsKif-SetsKif-ListsKif-Numbers

Generic-Bibliography

**Can-Be-One-Of****Can-Have-One****Cannot-Have****Has-At-Least****Has-At-Most****Has-One****Has-One-Of-Type****Has-Single-Slot-Value-Of-Type****Has-Slot-Value****Has-Slot-Value-Of-Type****Has-Some****Has-Value-Of-Type****Has-Values****Have-Same-Slot-Values****Have-Same-Values****Must-Be-One-Of****Value-Class**

**The following constants were used from included theories:**

**=<***defined as a***relation***in theory***Kif-Numbers****>=***defined as a***relation***in theory***Kif-Numbers****Alias***defined as a***relation***in theory***Frame-Ontology****Arity***defined as a***function***in theory***Frame-Ontology****Binary-Relation***defined as a***class***in theory***Kif-Relations****Binary-Relation***defined as a***class***in theory***Frame-Ontology****Class***defined as a***class***in theory***Frame-Ontology****Compose***defined as a***function***in theory***Frame-Ontology****Documentation***defined as a***relation***in theory***Frame-Ontology****Exact-Domain***defined as a***function***in theory***Frame-Ontology****Function***defined as a***class***in theory***Kif-Relations****Function***defined as a***class***in theory***Frame-Ontology****Has-Value***defined as a***relation***in theory***Frame-Ontology****Holds***defined as a***relation***in theory***Kif-Relations****Instance-Of***defined as a***relation***in theory***Frame-Ontology****Member***defined as a***relation***in theory***Kif-Sets****Natural***defined as a***class***in theory***Kif-Numbers****Nth-Domain***defined as a***relation***in theory***Frame-Ontology****Range***defined as a***relation***in theory***Frame-Ontology****Relation***defined as a***class***in theory***Kif-Relations****Relation***defined as a***class***in theory***Frame-Ontology****Same-Slot-Values***defined as a***relation***in theory***Frame-Ontology****Same-Values***defined as a***relation***in theory***Frame-Ontology****Set***defined as a***class***in theory***Kif-Sets****Single-Valued-Slot***defined as a***relation***in theory***Frame-Ontology****Subrelation-Of***defined as a***relation***in theory***Frame-Ontology****Undefined***defined as a***class***in theory***Kif-Relations****Value-Cardinality***defined as a***function***in theory***Frame-Ontology****Value-Type***defined as a***relation***in theory***Frame-Ontology**

**All constants that were mentioned were defined.**

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.

**Arity:**3

**Axioms:**

(Nth-Domain Has-Values 3 Set) (Nth-Domain Has-Values 2 Binary-Relation) (<=> (Has-Values ?Instance ?Binary-Relation ?Set-Of-Values) (And (Binary-Relation ?Binary-Relation) (Set ?Set-Of-Values) (Forall (?Instance) (<=> (Member ?Instance ?Set-Of-Values) (Has-Value ?Instance ?Binary-Relation ?Value) ))))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Alias:**Same-values**Arity:**3

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3

**Axioms:**

(Nth-Domain Has-At-Least 3 Natural) (Nth-Domain Has-At-Least 2 Binary-Relation) (<=> (Has-At-Least ?Instance ?Binary-Relation ?N) (And (Binary-Relation ?Binary-Relation) (Natural ?N) (>= (Value-Cardinality ?Instance ?Binary-Relation) ?N) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3

**Axioms:**

(Nth-Domain Has-At-Most 3 Natural) (Nth-Domain Has-At-Most 2 Binary-Relation) (<=> (Has-At-Most ?Instance ?Binary-Relation ?N) (And (Binary-Relation ?Binary-Relation) (Natural ?N) (=< 0 (Value-Cardinality ?Instance ?Binary-Relation) ?N) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2**Range:**Binary-relation

**Axioms:**

(<=> (Has-One ?Instance ?Binary-Relation) (And (Binary-Relation ?Binary-Relation) (= (Value-Cardinality ?Instance ?Binary-Relation) 1) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2

**Axioms:**

(<=> (Has-Some ?Instance ?Binary-Relation) (Has-At-Least ?Instance ?Binary-Relation 1) )

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2

**Axioms:**

(<=> (Can-Have-One ?Instance ?Binary-Relation) (Has-At-Most ?Instance ?Binary-Relation 1) )

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2

**Axioms:**

(<=> (Cannot-Have ?Instance ?Binary-Relation) (Not (Instance-Of ?Instance (Exact-Domain ?Binary-Relation))) )

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3**Subrelation-Of:**Value-type

**Axioms:**

(Nth-Domain Has-Value-Of-Type 3 Class) (Nth-Domain Has-Value-Of-Type 2 Binary-Relation) (<=> (Has-Value-Of-Type ?Instance ?Binary-Relation ?Type) (And (Binary-Relation ?Binary-Relation) (Class ?Type) (>= (Value-Cardinality ?Instance ?Binary-Relation) 1) (Value-Type ?Instance ?Binary-Relation ?Type) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3**Subrelation-Of:**Value-type

**Axioms:**

(Nth-Domain Has-One-Of-Type 3 Class) (Nth-Domain Has-One-Of-Type 2 Binary-Relation) (<=> (Has-One-Of-Type ?Instance ?Binary-Relation ?Type) (And (Binary-Relation ?Binary-Relation) (Class ?Type) (= (Value-Cardinality ?Instance ?Binary-Relation) 1) (Value-Type ?Instance ?Binary-Relation ?Type) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

A class C HAS-SLOT-VALUE v of relation R if for every instance i of C, R(i,v).

**Arity:**3

**Axioms:**

(Nth-Domain Has-Slot-Value 2 Binary-Relation) (Nth-Domain Has-Slot-Value 1 Class) (<=> (Has-Slot-Value ?Class ?Binary-Relation ?Slot-Value) (And (Class ?Class) (Binary-Relation ?Binary-Relation) (=> (Instance-Of ?Instance ?Class) (Holds ?Binary-Relation ?Class ?Slot-Value) )))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3

**Axioms:**

(Nth-Domain Has-Slot-Value-Of-Type 3 Class) (Nth-Domain Has-Slot-Value-Of-Type 2 Binary-Relation) (Nth-Domain Has-Slot-Value-Of-Type 1 Class) (<=> (Has-Slot-Value-Of-Type ?Domain-Class ?Relation ?Type) (And (Class ?Domain-Class) (Binary-Relation ?Relation) (Class ?Type) (=> (Instance-Of ?Instance ?Domain-Class) (Has-Value-Of-Type ?Instance ?Relation ?Type) )))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**3**Subrelation-Of:**Has-slot-value-of-type

**Axioms:**

(Nth-Domain Has-Single-Slot-Value-Of-Type 3 Class) (Nth-Domain Has-Single-Slot-Value-Of-Type 2 Binary-Relation) (Nth-Domain Has-Single-Slot-Value-Of-Type 1 Class) (<=> (Has-Single-Slot-Value-Of-Type ?Class ?Binary-Relation ?Type) (And (Class ?Class) (Binary-Relation ?Binary-Relation) (Class ?Type) (Single-Valued-Slot ?Class ?Binary-Relation) (Has-Slot-Value-Of-Type ?Class ?Binary-Relation ?Type) ))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Alias:**Same-slot-values**Arity:**3

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2

**Axioms:**

(<=> (Can-Be-One-Of ?Instance ?Set-Of-Classes) (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))))))))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

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.

**Arity:**2**Subrelation-Of:**Can-be-one-of

**Axioms:**

(<=> (Must-Be-One-Of ?Instance ?Set-Of-Classes) (And (Can-Be-One-Of ?Instance ?Set-Of-Classes) (Exists (?Class) (And (Member ?Class ?Set-Of-Classes) (Instance-Of ?Instance ?Class) ))))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

Alias of COMPOSE, kept around for compatability.

**Alias:**Compose

**Axioms:**

(Undefined (Arity Compose*))

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

**Alias:**Value-type**Arity:**3

**Defined in theory: Slot-constraint-sugar****Source code: slot-constraint-sugar.lisp**

Formatting and translation code was written by