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 classes defined.

17 relations defined:

1 function defined:

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