# Theory SLOT-CONSTRAINT-SUGAR

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.

### Theories included by Slot-Constraint-Sugar:

```    Frame-Ontology
Kif-Relations
Kif-Sets
Kif-Lists
Kif-Numbers```

### Theories that include Slot-Constraint-Sugar:

`    Generic-Bibliography`

### No instances defined.

The following constants were used from included theories:

All constants that were mentioned were defined.

## Relation HAS-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.

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) ))))

```

## Relation HAVE-SAME-VALUES

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

## Relation HAS-AT-LEAST

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) ))

```

## Relation HAS-AT-MOST

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) ))

```

## Relation HAS-ONE

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) ))

```

## Relation HAS-SOME

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) )

```

## Relation CAN-HAVE-ONE

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) )

```

## Relation CANNOT-HAVE

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))) )

```

## Relation HAS-VALUE-OF-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.
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) ))

```

## Relation HAS-ONE-OF-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.
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) ))

```

## Relation HAS-SLOT-VALUE

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) )))

```

## Relation HAS-SLOT-VALUE-OF-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.
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) )))

```

## Relation HAS-SINGLE-SLOT-VALUE-OF-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.
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) ))

```

## Relation HAVE-SAME-SLOT-VALUES

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

## Relation CAN-BE-ONE-OF

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))))))))

```

## Relation MUST-BE-ONE-OF

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) ))))

```

## Function COMPOSE*

Alias of COMPOSE, kept around for compatability.
Alias: Compose
Axioms:
```(Undefined (Arity Compose*))

```

## Relation VALUE-CLASS

Alias: Value-type
Arity: 3

This document was generated using Ontolingua.
Formatting and translation code was written by
François Gerbaux and Tom Gruber