The Generic Frame Protocol provides operations for manipulating
knowledge expressed in an implicit representation formalism called the
*GFP Knowledge Model*, which we specify in this chapter. The GFP
Knowledge Model supports an object-oriented representation of knowledge
and provides a set of representational constructs commonly found in
frame representation systems (FRSs) [[7]]. Knowledge
obtained from an FRS using GFP or provided to an FRS using GFP is
assumed in the specification of the GFP operations to be expressed in
the Knowledge Model. The GFP Knowledge Model therefore serves as an
implicit *interlingua* for knowledge that is being communicated
using GFP, and systems that use GFP translate knowledge into and out of
that interlingua as needed.

The GFP Knowledge Model includes constants, frames, slots, facets, classes, individuals, and knowledge bases. We describe each of these constructs in the sections below. In order to provide a precise and succinct description of the GFP Knowledge Model, we use the Knowledge Interchange Format (KIF) [[4]] as a formal specification language. KIF is a first-order predicate logic language with set theory, and has a linear prefix syntax.

The GFP Knowledge Model assumes a universe of discourse consisting of
all entities about which knowledge is to be expressed. Each GFP
knowledge base may have a different universe of discourse.
However, GFP assumes that the universe of discourse always includes all
constants of the following *basic types*:

- integers
- floating point numbers
- strings
- symbols
- lists
- classes

Classes are sets of entities, and all sets of entities are considered to be
classes. GFP also assumes that the domain of discourse includes the
logical constants `true` and `false`.

A *frame* is a primitive object that represents an entity in the
domain of discourse. Formally, a frame corresponds to a KIF constant.
A frame that represents a class is called a *class frame*, and a
frame that represents an individual is called an *individual frame*.

A frame has associated with it a set of *own slots*, and each own
slot of a frame has associated with it a set of entities called *
slot values*. Formally, a slot is a binary relation, and each value V
of an own slot S of a frame F represents the assertion that the relation
S holds for the entity represented by F and the entity represented by V
(i.e., `(S F V)`). For example,
the assertion that Fred's favorite foods are potato chips and ice cream
could be represented by the own slot `Favorite-Food` of the frame
`Fred` having as values the frame `Potato-Chips` and the string
```ice cream''`.

An own slot of a frame has associated with it a set of *own facets*,
and each own facet of a slot of a frame has associated with it a set of
entities called *facet values*. Formally, a facet is a ternary
relation, and each value V of own facet Fa of slot S of frame Fr
represents the assertion that the relation Fa holds for the relation S,
the entity represented by Fr, and the entity represented by V (i.e.,
`(Fa S Fr V)`). For example, the assertion that the favorite foods
of Fred must be edible foods could be represented by the facet
`:VALUE-TYPE` of the `Favorite-Food` slot of the `Fred` frame
having the value `Edible-Food`.

Relations may optionally be entities in the domain of discourse and
therefore representable by frames. Thus, a slot or a facet may be
represented by a frame. Such a frame describes the properties of the
relation represented by the slot or facet. A frame representing a slot
is called a *slot frame*, and a frame representing a facet is called
a *facet frame*.

A *class* is a set of entities. Each of the entities in a class is
said to be an *instance of* the class. An entity can be an instance
of multiple classes, which are called its *types*. A class can be
an instance of a class. A class which has instances that are themselves
classes is called a *meta-class*.

Entities that are not classes are referred to as *individuals*.
Thus, the domain of discourse consists of individuals and classes. The
unary relation `class` is true if and only if its argument is a
class and the unary relation `individual` is true if and only if its
argument is an individual. The following axiom holds:

(<=> (class ?X) (not (individual ?X)))

The class membership relation (called *instance-of*) that holds
between an instance and a class is a binary relation that maps
entities to classes. A class is considered to be a unary relation
that is true for each instance of the class. That is,

(<=> (holds ?C ?I) (instance-of ?I ?C))

The relation *type-of* is defined as the inverse of relation `
instance-of`. That is,

(<=> (type-of ?C ?I) (instance-of ?I ?C))

The *subclass-of* relation for classes is defined in terms of the
relation `instance-of`, as follows. A class Csub is a subclass of
class Csuper if
and only if all instances of Csub are also instances of Csuper. That
is,

(<=> (subclass-of ?Csub ?Csuper) (forall ?I (=> (instance-of ?I ?Csub) (instance-of ?I ?Csuper))))

Note that this definition implies that `subclass-of` is transitive.
(I.e., If A is a subclass of B and B is a subclass of C, then A is a
subclass of C.)

The relation *superclass-of* is defined as the inverse of the
relation `subclass-of`. That is,

(<=> (superclass-of ?Csuper ?Csub) (subclass-of ?Csub ?Csuper))

A class frame has associated with it a collection of *template
slots* that describe own slot values considered to hold for each
instance of the class represented by the frame. The values of
template slots are said to *inherit* to the subclasses and to the
instances of a class. Formally, each value V of a template slot S of
a class frame C represents the assertion that the relation *
template-slot-value* holds for the relation S, the class represented
by C, and the entity represented by V (i.e., `(template-slot-value
S C V)`). That assertion, in turn, implies that the relation S holds
between each instance I of class C and value V (i.e., `(S I V)`).
It also implies that the relation `template-slot-value` holds for
the relation S, each subclass Csub of class C, and the entity
represented by V (i.e., `(template-slot-value S Csub V)`). That
is, the following *slot value inheritance axiom* holds for the relation `template-slot-value`:

(=> (template-slot-value ?S ?C ?V) (and (=> (instance-of ?I ?C) (holds ?S ?I ?V)) (=> (subclass-of ?Csub ?C) (template-slot-value ?S ?Csub ?V))))

Thus, the values of a template slot are inherited to subclasses as
values of the same template slot and to instances as values of the
corresponding own slot. For example, the assertion that the gender of
all female persons is female could be represented by template slot `
Gender` of class frame `Female-Person` having the value `
Female`. Then, if we created an instance of `Female-Person` called
`Mary`, `Female` would be a value of the own slot `Gender`
of `Mary`.

A template slot of a class frame has associated with it a collection of
*template facets* that describe own facet values considered to hold
for the corresponding own slot of each instance of the class represented
by the class frame. As with the values of template slots, the values of
template facets are said to inherit to the subclasses and instances of a
class. Formally, each value V of a template facet F of a template slot
S of a class frame C represents the assertion that the relation *
template-facet-value* holds for the relations F and S, the class
represented by C, and the entity represented by V (i.e., `
(template-facet-value F S C V)`). That assertion, in turn, implies that
the relation F holds for relation S, each instance I of class C, and
value V (i.e., `(F S I V)`). It also implies that the relation `
template-facet-value` holds for the relations S and F, each subclass
Csub of class C, and the entity represented by V (i.e., `
(template-facet-value F S Csub V)`).

In general, the following *facet value inheritance axiom*
holds for the relation `
template-facet-value`:

(=> (template-facet-value ?F ?S ?C ?V) (and (=> (instance-of ?I ?C) (holds ?F ?S ?I ?V)) (=> (subclass-of ?Csub ?C) (template-facet-value ?F ?S ?Csub ?V))))

Thus, the values of a template facet are inherited to subclasses as values of the same template facet and to instances as values of the corresponding own facet.

Note that template slot values and template facet values *
necessarily* inherit from a class to its subclasses and instances.
Default values and default inheritance are specified separately, as
described in Section 2.8.

Classes are considered to be either *primitive* or *
non-primitive* by GFP. The template slot values and template facet
values associated with a non-primitive class are considered to specify a
set of necessary *and sufficient* conditions for being an instance
of the class. For example, the class `Triangle` could be a
non-primitive class whose template slots and facets specify three-sided
polygons. All triangles are necessarily three-sided polygons, and
knowing that an entity is a three-sided polygon is sufficient to
conclude that the entity is a triangle.

The template slot values and template facet values associated with a
primitive class are considered to specify only a set of necessary
conditions for an instance of the class. For example, all classes
of ``natural kinds'' - such as `Horse` and `Building` - are
primitive concepts. A KB may specify many properties of horses and
buildings, but will typically not contain sufficient conditions for
concluding that an entity is a horse or building.

Formally:

(=> (and (class ?C) (not (primitive ?C))) (=> (and (=> (template-slot-value ?S ?C ?V) (holds ?S ?I ?V)) (=> (template-facet-value ?F ?S ?C ?V) (holds ?F ?S ?I ?V))) (instance-of ?I ?C)))

Each frame has associated with it a collection of slots, and each
frame-slot pair has associated with it a collection of facets. A facet
is considered to be associated with a frame-slot pair if the facet has a
value for the slot at the frame. A slot is considered to be associated
with a frame if the slot has a value at that frame or there is a facet
that is associated with the slot at the frame. For example, if the
template facet `:NUMERIC-MINIMUM` of template slot `Age` of
frame `Person` had a value `0`, then facet `:NUMERIC-MINIMUM` would be associated with the frame `Person` slot
`Age` pair and the slot `Age` would be associated with the frame
`Person`. In addition, GFP contains operations for explicitly
associating slots with frames and associating facets with frame-slot
pairs, even though there are no values for the slots or facets at the
frame.

We formalize the association of slots with frames and facets with
frame-slot pairs by defining the relations `slot-of`, `
template-slot-of`, `facet-of`, and `template-facet-of` as
follows:

(=> (exists ?V (holds ?Fa ?S ?F ?V)) (facet-of ?Fa ?S ?F)) (=> (exists ?V (template-facet-value ?Fa ?S ?C ?V)) (template-facet-of ?Fa ?S ?C)) (=> (or (exists ?V (holds ?S ?F ?V)) (exists ?Fa (facet-of ?Fa ?S ?F))) (slot-of ?S ?F)) (=> (or (exists ?V (template-slot-value ?S ?C ?V)) (exists ?Fa (template-facet-of ?Fa ?S ?C))) (template-slot-of ?S ?C))

So, in the example given above, the following sentences would be true:
`(template-slot-of Age Person)` and `(template-facet-of
:NUMERIC-MINIMUM Age Person)`.

As with template facet values and template slot values, the `
template-slot-of` and `template-facet-of` relations inherit from a
class to its subclasses and from a class to its instances as the `
slot-of` and `facet-of` relations. That is, the following slot-of
inheritance axioms hold.

(=> (template-slot-of ?S ?C) (and (=> (instance-of ?I ?C) (slot-of ?S ?I)) (=> (subclass-of ?Csub ?C) (template-slot-of ?S ?Csub)))) (=> (template-facet-of ?Fa ?S ?C) (and (=> (instance-of ?I ?C) (facet-of ?Fa ?S ?I)) (=> (subclass-of ?Csub ?C) (template-facet-of ?Fa ?S ?Csub))))

GFP allows multiple values of a slot or facet to be interpreted as a
collection type other than a set. The protocol recognizes three
collection types: *set*, *bag*, and *list*. A bag is an
unordered collection with possibly multiple occurrences of the same
value in the collection. A list is an ordered
bag.

The GFP Knowledge Model considers multiple slot and facet values to be
sets throughout because of the lack of a suitable formal interpretation
for (1)
multiple slot or facet values treated as bags or lists, (2) the ordering
of values in lists of values that result from multiple inheritance, and
(3) the multiple occurrence of values in bags that result from multiple
inheritance. In addition, the protocol itself makes no commitment as to
how values expressed in collection types other than `set` are
combined during inheritance. Thus, GFP guarantees that multiple slot
and facet values of a frame stored as a bag or a list are retrievable as
an equivalent bag or list *at that frame*. However, when the values
are inherited to a subclass or instance, no guarantees are provided
regarding the ordering of values for lists or the repeating of multiple
occurrences of values for bags. The collection types supported by an
FRS can be specified by a behavior (see
Section 4.1.7) and the collection type of a
slot of a specific frame can be specified by using the `
:COLLECTION-TYPE` facet (see Section 2.10.2).

The GFP knowledge model includes a simple provision for default values
for slots and facets. Template slots and template facets have a set of
*default values* associated with them. Intuitively, these default
values inherit to instances unless the inherited values are logically
inconsistent with other assertions in the KB, the values have been
removed at the instance, or the default values have been explicitly
overridden by other default values. GFP does not require an FRS to be
able to determine the logical consistency of a KB, nor does it provide a
means of explicitly overriding default values. Instead, GFP leaves the
inheritance of default values unspecified. That is, no requirements are
imposed on the relationship between default values of template slots and
facets and the values of the corresponding own slots and facets. The
default values on a template slot or template facet are simply available
to the FRS to use in whatever way it chooses when determining the values
of own slots and facets. GFP guarantees that, unless the value of the
`:default` behavior is `:none`, default values for a template
slot or template facet asserted at a class frame will be retrievable
*at that
frame*. However, no guarantees are made as to how or whether the
default values are inherited to a subclass or instance.

A *knowledge base* (KB) is a collection of classes, individuals,
frames, slots, slot values, facets, facet values, frame-slot
associations, and frame-slot-facet associations. KBs are considered to
be entities in the universe of discourse and are represented by frames.
All frames reside in some KB. The frames representing KBs are
considered to reside in a distinguished KB called the *meta-kb*,
which is accessible to GFP applications.

The GFP Knowledge Model includes a collection of classes, facets, and slots with specified names and semantics. It is not required that any of these standard classes, facets, or slots be represented in any given KB, but if they are, they must satisfy the semantics specified here.

The purpose of these standard names is to allow for FRS- and KB-independent canonical names for frequently used classes, facets, and slots. The canonical names are needed because an application cannot in general embed literal references to frames in a KB and still be portable. This mechanism enables such literal references to be used without compromising portability.

Whether the classes described in this section are actually present in a
KB or not, GFP guarantees that all of these class names are valid values
for the `:VALUE-TYPE` facet described in
Section 2.10.2.

`:THING` *class*

`:THING` is the root of the class hierarchy for a KB, meaning that
`:THING` is the superclass of every class in every KB.

`:CLASS` *class*

`:CLASS` is the class of all classes. That is, every entity that is
a class is an instance of `:CLASS` .

`:INDIVIDUAL` *class*

`:INDIVIDUAL` is the class of all entities that are not classes.
That is, every entity that is not a class is an instance of `:INDIVIDUAL` .

`:NUMBER` *class*

`:NUMBER` is the class of all numbers. GFP makes no guarantees
about the precision of numbers. If precision is an issue for an
application, then the application is responsible for maintaining and
validating the format of numerical values of slots and facets.
`:NUMBER` is a subclass of `:INDIVIDUAL` .

`:INTEGER` *class*

`:INTEGER` is the class of all integers and is a subclass of
`:NUMBER` . As with numbers in general, GFP makes no guarantees about the
precision of integers.

`:STRING` *class*

`:STRING` is the class of all text strings. `:STRING` is a
subclass of `:INDIVIDUAL` .

`:SYMBOL` *class*

`:SYMBOL` is the class of all symbols. `:SYMBOL` is a subclass
of `:SEXPR` .

`:LIST` *class*

`:LIST` is the class of all lists. `:LIST` is a subclass of
`:INDIVIDUAL` .

The standard facet names in GFP have been derived from the Knowledge
Representation System Specification (`KRSS`) [[13]] and the
Ontolingua Frame Ontology. `KRSS` is a common denominator for
description logic systems such as LOOM [[12]], CLASSIC\
[[2]], and BACK [[14]]. The Ontolingua Frame
Ontology defines a frame language as an extension to KIF. KIF plus the
Ontolingua Frame Ontology is the representation language used in
Stanford University's Ontolingua System [[5]]. Both KRSS
and Ontolingua were developed as part of DARPA's Knowledge Sharing
Effort.

`:VALUE-TYPE` *facet*

The `:VALUE-TYPE` facet specifies a type restriction on the values
of a slot of a frame. Each value of the `:VALUE-TYPE` facet denotes
a class. A value C for facet `:VALUE-TYPE` of slot S of frame F
means that every value of slot S of frame F must be an instance of the
class C. That is,

(=> (:VALUE-TYPE ?S ?F ?C) (and (class ?C) (=> (holds ?S ?F ?V) (instance-of ?V ?C)))) (=> (template-facet-value :VALUE-TYPE ?S ?F ?C) (and (class ?C) (=> (template-slot-value ?S ?F ?V) (instance-of ?V ?C))))

The first axiom provides the semantics of the `:VALUE-TYPE` facet
for
own slots and the second provides the semantics for template slots.
Note that if the `:VALUE-TYPE` facet has multiple values for a slot
S of a frame F, then the values of slot S of frame F must be an instance
of *every* class
denoted by the values of `:VALUE-TYPE` .

A value for `:VALUE-TYPE` can be a KIF term of the following form:

<value-type-expr> ::= (union <gfp-class>*) | (set-of <gfp-value>*) | gfp-class

A `gfp-class` is any entity `X` for which `(class X)`
is `true` or that is a standard GFP class described in
Section 2.10.1. A `gfp-value` is any entity. The
`union` expression allows the specification of a disjunction of
classes (e.g., either a dog or a cat), and the `set-of` expression
allows the specification of an explicitly enumerated set of possible
values for the slot (e.g., either Clyde, Fred, or Robert).

`:INVERSE` *facet*

The `:INVERSE` facet of a slot of a frame specifies inverses
for that slot for the values of the slot of the frame. Each value of
this facet is a slot. A value S2 for facet `:INVERSE` of slot
S1 of frame F means that if V is a value of S1 of F, then F is a value
of S2 of V. That is,

(=> (:INVERSE ?S1 ?F ?S2) (and (:SLOT ?S2) (=> (holds ?S1 ?F ?V) (holds ?S2 ?V ?F)))) (=> (template-facet-value :INVERSE ?S1 ?F ?S2) (and (:SLOT ?S2) (=> (template-slot-value ?S1 ?F ?V) (template-slot-value ?S2 ?V ?F))))

`:CARDINALITY` *facet*

The `:CARDINALITY` facet specifies the exact number of values that
may be asserted for a slot on a frame. The value of this facet must be a
nonnegative integer. A value N for facet `:CARDINALITY` on slot S
on frame F means that slot S on frame F has N values. That
is,

(=> (:CARDINALITY ?S ?F ?N) (= (cardinality (setofall ?V (holds ?S ?F ?V))) ?N)) (=> (template-facet-value :CARDINALITY ?S ?F ?C) (=< (cardinality (setofall ?V (template-slot-value ?S ?F ?V)) ?N)))

For example, one could represent the assertion that Fred has exactly
four brothers by asserting 4 as the value of the `:CARDINALITY` own
facet of the `Brother` own slot of frame `Fred`. Note that
all the values for slot S of frame F need not be known in the KB.
That is, a KB could use the `:CARDINALITY` facet to specify that
Fred has 4 brothers without knowing who the brothers are and therefore
without providing values for Fred's `Brother` slot.

Also, note that a value for `:CARDINALITY` as a template facet of a
template slot of a class only constrains the maximum number of values
of that
template slot of that class, since the corresponding own slot of each
instance of the class may inherit values from multiple classes and have
locally asserted values.

`:MAXIMUM-CARDINALITY` *facet*

The `:MAXIMUM-CARDINALITY` facet specifies the maximum number of
values that may be asserted for a slot of a frame. Each value of this
facet must be a nonnegative integer. A value N for facet `
MAXIMUM-CARDINALITY` of slot S of frame F means that slot S of frame F
can have at most N values. That is,

(=> (:MAXIMUM-CARDINALITY ?S ?F ?N) (=< (cardinality (setofall ?V (holds ?S ?F ?V))) ?N)) (=> (template-facet-value :MAXIMUM-CARDINALITY ?S ?F ?C) (=< (cardinality (setofall ?V (template-slot-value ?S ?F ?V)) ?N)))

Note that if facet `:MAXIMUM-CARDINALITY` of a slot S of a frame F
has multiple values N1, ,Nk, then S in F can have at most `
(min N1 Nk)` values. Also, it is appropriate for a value for
`:MAXIMUM-CARDINALITY` as a template facet of a template slot of a class
to constrain the number of values of that template slot of that class as
well as the number of values of the corresponding own slot of each
instance of that class since an excess of values for a template slot of
a class will cause an excess of values for the corresponding own slot of
each instance of the class.

`:MINIMUM-CARDINALITY` *facet*

The `:MINIMUM-CARDINALITY` facet specifies the minimum number of
values that may be asserted for a slot of a frame. Each value of this
facet must be a nonnegative integer. A value N for facet `
MINIMUM-CARDINALITY` of slot S of frame F means that slot S of frame F
has at least N values. That is,

(=> (:MINIMUM-CARDINALITY ?S ?F ?N) (>= (cardinality (setofall ?V (holds ?S ?F ?V))) ?N))

Note that if facet `:MINIMUM-CARDINALITY` of a slot S of a frame F
has multiple values N1, ,Nk, then S of F has at least `(max
N1 Nk)` values. Also, as is the case with the `:CARDINALITY`
facet, all the values for slot S of frame F do not need be known in the
KB.

Note that a value for `:MINIMUM-CARDINALITY` as a template
facet of a template slot of a class does not constrain the number of
values of that template slot of that class, since the corresponding own
slot of each instance of the class may inherit values from multiple
classes and have locally asserted values. Instead, the value for the
template facet `:MINIMUM-CARDINALITY` constrains only the number of
values of the corresponding own slot of each instance of that class, as
specified by the axiom.

`:SAME-VALUES` *facet*

The `:SAME-VALUES` facet specifies that a slot of a frame has
the same values as other slots of that frame or as the values
specified by *slot chains* starting at that frame. Each value of
this facet is either a slot or a slot chain. A value S2 for facet
`:SAME-VALUES` of slot S1 of frame F, where S2 is a slot, means
that the set of values of slot S1 of F is equal to the set of values
of slot S2 of F. That is,

(=> (:SAME-VALUES ?S1 ?F ?S2) (= (setofall ?V (holds ?S1 ?F ?V)) (setofall ?V (holds ?S2 ?F ?V))))

A *slot chain* is a list of slots that specifies a nesting of
slots. That is, the values of the slot chain S1, ,Sn of frame F
are the values of
the Sn slot of the values of the Sn-1 slot of of the values of
the S1
slot in F. For example, the values of the slot chain `(parent
brother)` of `Fred` are the brothers of the parents of Fred.
Formally, we define the values of a slot chain recursively as follows:
Vn is a value of slot chain S1, ,Sn of frame F if there is a
value V1 of
slot S1 of F such that Vn is a value of slot chain S2, ,Sn of
frame V1.
That is,

(<=> (slot-chain-value (listof ?S1 ?S2 @Sn) ?F ?Vn) (exists ?V1 (and (holds ?S1 ?F ?V1) (slot-chain-value (listof ?S2 @Sn) ?V1 ?Vn)))) (<=> (slot-chain-value (listof ?S) ?F ?V) (holds ?S ?F ?V))

A value `(S1 Sn)` for facet `:SAME-VALUES` of slot S of
frame
F means that the set of values of slot S of F is equal to the set of
values of slot chain `(S1 Sn)` of F. That is,

(=> (:SAME-VALUES ?S ?F (listof @Sn)) (= (setofall ?V (holds ?S ?F ?V)) (setofall ?V (slot-chain-value (listof @Sn) ?F ?V))))

For example, one could assert that a person's uncles are the brothers of
their parents by putting the value `(parent brother)` on the
template
facet `:SAME-VALUES` of the `Uncle` slot of class `Person`.

`:NOT-SAME-VALUES` *facet*

The `:NOT-SAME-VALUES` facet specifies that a slot of a frame
does not have the same values as other slots of that frame or as the
values specified by slot chains starting at that frame. Each value of
this facet is either a slot or a slot chain. A value S2 for facet
`:NOT-SAME-VALUES` of slot S1 of frame F, where S2 is a slot,
means that the set of values of slot S1 of F is not equal to the set
of values of slot S2 of F. That is,

(=> (:NOT-SAME-VALUES ?S1 ?F ?S2) (not (= (setofall ?V (holds ?S1 ?F ?V)) (setofall ?V (holds ?S2 ?F ?V)))))

A value `(S1 Sn)` for facet `:NOT-SAME-VALUES` of slot
S of
frame F means that the set of values of slot S of F is not equal to the
set of values of slot chain `(S1 Sn)` of F. That is,

(=> (:NOT-SAME-VALUES ?S ?F (listof @Sn)) (not (= (setofall ?V (holds ?S ?F ?V)) (setofall ?V (slot-chain-value (listof @Sn) ?F ?V)))))

`:SUBSET-OF-VALUES` *facet*

The `:SUBSET-OF-VALUES` facet specifies that the values of a
slot of a frame are a subset of the values of other slots of that
frame or of the values of slot chains starting at that frame. Each
value of this facet is either a slot or a slot chain. A value S2 for
facet `:SUBSET-OF-VALUES` of slot S1 of frame F, where S2 is a
slot, means that the set of values of slot S1 of F is a subset of the
set of values of slot S2 of F. That is,

(=> (:SUBSET-OF-VALUES ?S1 ?F ?S2) (subset (setofall ?V (holds ?S1 ?F ?V)) (setofall ?V (holds ?S2 ?F ?V))))

A value `(S1 Sn)` for facet `:SUBSET-OF-VALUES` of slot
S of
frame F means that the set of values of slot S of F is a subset of the
set of values of the slot chain `(S1 Sn)` of F. That is,

(=> (:SUBSET-OF-VALUES ?S ?F (listof @Sn)) (subset (setofall ?V (holds ?S ?F ?V)) (setofall ?V (slot-chain-value (listof @Sn) ?F ?V))))

`:NUMERIC-MINIMUM` *facet*

The `:NUMERIC-MINIMUM` facet specifies a lower bound on the
values of a slot whose values are numbers. Each value of the
`:NUMERIC-MINIMUM` facet is a number. This facet is defined as
follows:

(=> (:NUMERIC-MINIMUM ?S ?F ?N) (and (:NUMBER ?N) (=> (holds ?S ?F ?V) (>= ?V ?N)))) (=> (template-facet-value :NUMERIC-MINIMUM ?S ?F ?N) (and (:NUMBER ?N) (=> (template-slot-value ?S ?F ?V) (>= ?V ?N))))

`:NUMERIC-MAXIMUM` *facet*

The `:NUMERIC-MAXIMUM` facet specifies an upper bound on the values
of a slot whose values are numbers. Each value of this facet is a
number. This facet is defined as follows:

(=> (:NUMERIC-MAXIMUM ?S ?F ?N) (and (:NUMBER ?N) (=> (holds ?S ?F ?V) (=< ?V ?N)))) (=> (template-facet-value :NUMERIC-MAXIMUM ?S ?F ?N) (and (:NUMBER ?N) (=> (template-slot-value ?S ?F ?V) (=< ?V ?N))))

`:SOME-VALUES` *facet*

The `:SOME-VALUES` facet specifies a subset of the values of a
slot of a frame. This facet of a slot of a frame can have any value
that can also be a value of the slot of the frame. A value V for own
facet `:SOME-VALUES` of own slot S of frame F means that V is
also a value of own slot S of F. That is,

(=> (:SOME-VALUES ?S ?F ?V) (holds ?S ?F ?V))

`:COLLECTION-TYPE` *facet*

The `:COLLECTION-TYPE` facet specifies whether multiple values of a
slot are to be treated as a set, list, or bag. No axiomatization is
provided for treating multiple values as lists or bags because of the
lack of a suitable formal interpretation for the ordering of values in
lists of values that result from multiple inheritance and the multiple
occurrence of values in bags that result from multiple inheritance.

The protocol itself makes no commitment as to how values expressed in
collection types other than `set` are combined during inheritance.
Thus,
GFP guarantees that multiple slot and facet values stored at a frame as
a bag or a list are retrievable as an equivalent bag or list *at
that frame*. However, when the values are inherited to a subclass or
instance, no guarantees are provided regarding the ordering of values
for lists or the repeating of multiple occurrences of values for bags.

`:DOCUMENTATION` *slot*

`:DOCUMENTATION` is a slot whose values at a frame are text strings
providing documentation for that frame. Note that the documentation
describing a class would be values of the *own slot* `:DOCUMENTATION`
on the class. The only requirement on the `:DOCUMENTATION` slot is
that its values be strings. That is,

(=> (:DOCUMENTATION ?F ?S) (:STRING ?S))

The slots described in this section can be associated with frames that represent slots. In general, these slots describe properties of a slot which hold at any frame that can have a value for the slot.

`:DOMAIN` *slot*

`:DOMAIN` specifies the domain of the binary relation represented by
a slot frame. Each value of the slot `:DOMAIN` denotes a class. A
slot frame S having a value C for own slot `:DOMAIN` means that
every frame that has a value for own slot S must be an instance of C,
and every frame that has a value for template slot S must be C or a
subclass of C. That is,

(=> (:DOMAIN ?S ?C) (and (:SLOT ?S) (class ?C) (=> (holds ?S ?F ?V) (instance-of ?F ?C)) (=> (template-slot-value ?S ?F ?V) (or (= ?F ?C) (subclass-of ?F ?C))))

If a slot frame S has a value C for own slot `:DOMAIN` and I is an
instance of C, then I is said to be *in the domain of* S.

A value for slot `:DOMAIN` can be a KIF expression of the following
form:

<domain-expr> ::= (union <gfp-class>*) | gfp-classA

Note that if slot `:DOMAIN` of a slot frame S has multiple
values C1, ,Cn, then the domain of slot S is constrained to be
the intersection of classes C1, ,Cn. Every slot is considered
to have `:THING` as a value of its `:DOMAIN` slot. That
is,

(=> (:SLOT ?S) (:DOMAIN ?S :THING))

`:SLOT-VALUE-TYPE` *slot*

`:SLOT-VALUE-TYPE` specifies the classes of which values of a slot
must be an instance (i.e., the range of the binary relation
represented by a slot). Each value of the slot
`:SLOT-VALUE-TYPE` denotes a class. A slot frame S having a
value V for own slot `:SLOT-VALUE-TYPE` means that the own facet
`:VALUE-TYPE` has value V for slot S of any frame that is in the
domain of S. That is,

(=> (:SLOT-VALUE-TYPE ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:VALUE-TYPE ?S ?F ?V))))

As is the case for the `:VALUE-TYPE` facet, the value for the
`:SLOT-VALUE-TYPE` slot can be a KIF expression of the following
form:

<value-type-expr> ::= (union <gfp-class>*) | (set-of <gfp-value>*) | gfp-class

A `gfp-class` is any entity `X` for which `(class X)`
is `true` or that is a standard GFP class described in
Section 2.10.1. A `gfp-value` is any entity. The
`union` expression allows the specification of a disjunction of
classes (e.g., either a dog or a cat), and the `set-of` expression
allows the specification of an explicitly enumerated set of values
(e.g., either Clyde, Fred, or Robert).

`:SLOT-INVERSE` *slot*

`:SLOT-INVERSE` specifies inverse relations for a slot. Each value
of `:SLOT-INVERSE` is a slot. A slot frame S having a value V for
own slot `:SLOT-INVERSE` means that own facet `:INVERSE` has
value V for slot S of any frame that is in the domain of S. That is,

(=> (:SLOT-INVERSE ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:INVERSE ?S ?F ?V))))

`:SLOT-CARDINALITY` *slot*

`:SLOT-CARDINALITY` specifies the exact number of values that may be
asserted for a slot for entities in the slot's domain. The value of
slot `:SLOT-CARDINALITY` is a nonnegative integer. A slot frame S
having a value V for own slot `:SLOT-CARDINALITY` means that own
facet `:CARDINALITY` has value V for slot S of any frame that is in
the domain of S. That is,

(=> (:SLOT-CARDINALITY ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:CARDINALITY ?S ?F ?V))))

`:SLOT-MAXIMUM-CARDINALITY` *slot*

`:SLOT-MAXIMUM-CARDINALITY` specifies the maximum number of values
that may be asserted for a slot for entities in the slot's domain.
The value of slot `:SLOT-MAXIMUM-CARDINALITY` is a nonnegative
integer. A slot frame S having a value V for own slot
`:SLOT-MAXIMUM-CARDINALITY` means that own facet
`:MAXIMUM-CARDINALITY` has value V for slot S of any frame that
is in the domain of S. That is,

(=> (:SLOT-MAXIMUM-CARDINALITY ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:MAXIMUM-CARDINALITY ?S ?Csub ?V))))

`:SLOT-MINIMUM-CARDINALITY` *slot*

`:SLOT-MINIMUM-CARDINALITY` specifies the minimum number of values
for a slot for entities in the slot's domain. The value of slot
`:SLOT-MINIMUM-CARDINALITY` is a nonnegative integer. A slot
frame S having a value V for own slot
`:SLOT-MINIMUM-CARDINALITY` means that own facet
`:MINIMUM-CARDINALITY` has value V for slot S of any frame that
is in the domain of S. That is,

(=> (:SLOT-MINIMUM-CARDINALITY ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:MINIMUM-CARDINALITY ?S ?F ?V))))

`:SLOT-SAME-VALUES` *slot*

`:SLOT-SAME-VALUES` specifies that a slot has the same values as
either other slots or as slot chains for entities in the slot's domain.
Each value of slot `:SLOT-SAME-VALUES` is either a slot or a slot
chain. A slot frame S having a value V for own slot
`:SLOT-SAME-VALUES` means that own facet `:SAME-VALUES`
has value V for slot S of any frame that is in the domain of S. That is,

(=> (:SLOT-SAME-VALUES ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:SAME-VALUES ?S ?F ?V)))

`:SLOT-NOT-SAME-VALUES` *slot*

`:SLOT-NOT-SAME-VALUES` specifies that a slot does not have the same
values as either other slots or as slot chains for entities in the
slot's domain. Each value of slot `:SLOT-NOT-SAME-VALUES` is either
a slot or a slot chain. A slot frame S having a value V for own slot
`:SLOT-NOT-SAME-VALUES` means that own facet `:NOT-SAME-VALUES`
has value V for slot S of any frame that is in the domain of S. That
is,

(=> (:SLOT-NOT-SAME-VALUES ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:NOT-SAME-VALUES ?S ?F ?V)))

`:SLOT-SUBSET-OF-VALUES` *slot*

`:SLOT-SUBSET-OF-VALUES` specifies that the values of a slot are a
subset of either other slots or of slot chains for entities in the
slot's domain. Each value of slot `:SLOT-SUBSET-OF-VALUES` is
either a slot or a slot chain. A slot frame S having a value V for
own slot `:SLOT-SUBSET-OF-VALUES` means that own facet
`:SUBSET-OF-VALUES` has value V for slot S of any frame that is
in the domain of S. That is,

(=> (:SLOT-SUBSET-OF-VALUES ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:SUBSET-OF-VALUES ?S ?F ?V)))

`:SLOT-NUMERIC-MINIMUM ` *slot*

`:SLOT-NUMERIC-MINIMUM` specifies a lower bound on the values of a
slot for entities in the slot's domain. Each value of slot
`:SLOT-NUMERIC-MINIMUM` is a number. A slot frame S having a
value V for own slot `:SLOT-NUMERIC-MINIMUM` means that own
facet `:NUMERIC-MINIMUM` has value V for slot S of any frame
that is in the domain of S. That is,

(=> (:SLOT-NUMERIC-MINIMUM ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:NUMERIC-MINIMUM ?S ?F ?V)))

`:NUMERIC-MAXIMUM-FOR-DOMAIN` *slot*

`:SLOT-NUMERIC-MAXIMUM` specifies an upper bound on the values of a
slot for entities in the slot's domain. Each value of slot
`:SLOT-NUMERIC-MAXIMUM` is a number. A slot frame S having a
value V for own slot `:SLOT-NUMERIC-MAXIMUM` means that own
facet `:NUMERIC-MAXIMUM` has value V for slot S of any frame
that is in the domain of S. That is,

(=> (:SLOT-NUMERIC-MAXIMUM ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:NUMERIC-MAXIMUM ?S ?F ?V)))

`:SLOT-SOME-VALUES` *slot*

`:SLOT-SOME-VALUES` specifies a subset of the values of a slot for
entities in the slot's domain. Each value of slot
`:SLOT-SOME-VALUES` of a slot frame must be in the domain of the
slot represented by the slot frame. A slot frame S having a value V
for own slot `:SLOT-SOME-VALUES` means that own facet
`:SOME-VALUES` has value V for slot S of any frame that is in
the domain of S. That is,

(=> (:SLOT-SOME-VALUES ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:SOME-VALUES ?S ?F ?V)))

`:SLOT-COLLECTION-TYPE` *slot*

`:SLOT-COLLECTION-TYPE` specifies whether multiple values of a slot
are to be treated as a set, list, or bag. Slot
`:SLOT-COLLECTION-TYPE` has one value, which is either `
set`, `list` or `bag`. A slot frame S having a value V for own slot
`:SLOT-COLLECTION-TYPE` means that own facet
`:COLLECTION-TYPE` has
value V for slot S of any frame that is in the domain of S. That is,

(=> (:SLOT-COLLECTION-TYPE ?S ?V) (and (:SLOT ?S) (=> (forall ?D (=> (:DOMAIN ?S ?D) (instance-of ?F ?D))) (:COLLECTION-TYPE ?S ?F ?V)))