Relation DOCUMENTATION


Slots on this relation:

Documentation:
Documentation is a relation between objects in the domain of discourse and strings of natural language text. The domain of DOCUMENTATION is not constants (names), but the objects themselves. This means that one does not quote the names when associating them with their documentation.
Instance-Of: Relation
Arity: 2
Range: String

Other Related Axioms:

(Documentation 
    Class
    A Class Can Be Thought Of As A Collection Of Individuals.
Formally, A Class Is A Unary Relation, A Set Of Tuples (Lists) Of
Length One.  Each Tuple Contains An Object Which Is Said To Be An
Instance Of The Class.  An Individual, Or Object, Is Any Identifiable
Entity In The Universe Of Discourse (Anything That Can Be Denoted By A
Object Constant In Kif), Including Classes Themselves.
  The Notion Of Class Is Introduced In Addition To The Relation
Vocabulary Because Of The Importance Of Classes And Types In Knowledge
Representation Practice.  The Notion Of Class And Relation Are Merged
To Unify Relational And Object-Centered Representational Conventions.
Classes Serve The Role Of `Sorts' And `Types'.
   There Is No First-Order Distinction Between Classes And Unary
Relations.  One Is Free To Define A Second-Order Predicate That Makes
The Distinction.  For Example, (Predicate C) Could Mean That The Unary
Relation C Should Be Thought Of More As A Property Than As A
Collection Of Individuals Over Which One Might Quantify Some
Statement.  Logically, All Such Predicates Would Still Be Instances Of
The Metaclass Class.
  The Fact That An Object I Is An Instance Of Class C Is Denoted By
The Sentence (C I).  One May Also Use The Equivalent Form
 (Instance-Of I C).  This Is Not Equivalent To (Member I C).
An Instance Of A Class Is Not A Set-Theoretic
Member Of The Class; Rather, The Tuple Containing The Instance Is A
Element Of The Set Of Tuples Which Is A Relation.
  The Definition Of A Class Is A Predicate Over A Single Free
Variable, Such That The Predicate Holds For Instances Of The Class.
In Other Words, Classes Are Defined _Intentionally_.  Two
Separately-Defined Classes May Have The Same Extension (In This Case
They Are = To Each Other).  It Is Possible To Define A Class By
Enumerating Its Instances, Using Kif'S Set Operations.  For Example,
  (Define-Class Primary-Color (?Color)
     (Member ?Color (Set Red Green Blue)))
)

(Documentation 
    Thing
    Thing Is The Class Of Everything In The Universe Of Discourse That
Can Be In A Class.  This Includes All The Relations And Objects
Defined In The Kif Specification, Plus All Other Objects Defined In
User Ontologies.  Every Thing Is Either A Simple-Set Or An Individual.
  There Are Entities In The Universe Of Discourse For Kif That Cannot
Be Instances Of Thing.  These Entities Are Unbounded Objects, Which By
Definition Cannot Be Members Of Any Set.  Since Thing Is A Class,
And Classes Are Relations, And Relations Are Sets, Then Unbounded
Entities Can'T Be Instances Of Any Class.
  That Is Why Thing Is Defined Here, As The Practical Root Of All
Ontologies.)

(Documentation 
    Individual-Thing
    An Individual-Thing Is Something That Isn'T A Set, But That
Can Be A Member Of A Set.  All Classes Of Things That Are Not Sets Are
Subclasses Of Individual-Thing.  The Kif Predicate Individual
Is True Of All Things That Are Not Sets, But This Includes
Entities That Can'T Be Members Of Any Set ("Unbounded" Entities).)

(Documentation 
    Instance-Of
    An Object Is An Instance-Of A Class If It Is A Member Of The Set
Denoted By That Class.  One Would Normally State The Fact That
Individual I Is An Instance Of Class C With With The Relational 
Form (C I), But It Is Equivalent To Say (Instance-Of I C).  
Instance-Of Is Useful For Defining The Second-Order Relations And
Classes That Are About Class/Instance Networks.
  An Individual May Be An Instance Of Many Classes, Some Of Which May Be
Subclasses Of Others.  Thus, There Is No Assumption In The Meaning
Of Instance-Of About Specificity Or Uniqueness.  See
Direct-Instance-Of.)

(Documentation Has-Instance The inverse relation for INSTANCE-OF.)

(Documentation 
    All-Instances
    The Instances Of Some Classes May Be Specified Extensionally.  That
Is, One Can List All Of The Instances Of The Class By Definition.  For
This Case We Say (= (All-Instances C) (Setof V_1 V_2 ...  V_N)), Where
C Is A Class And The V_I Are Its Instances.
  All-Instances Imposes A Monotonic Constraint. Any Subclass Of C
Cannot Have Any Instances Outside Of The All-Instances Of C.
Note That This Is Not Indexical Or Modal: Whether Something Is In 
All-Instances Is A Property Of The Modeled World And Does Not Depend
On The Facts Currently Stored In Some Knowledge Base.)

(Documentation 
    One-Of
    One-Of Is A Function For Defining Classes By Enumerating 
Their Instances.   It Takes A Variable Number Of Terms As Arguments, 
And Denotes The Class Whose Instances Are Exactly Those Terms.
   For Example, (One-Of Yes No) Denotes The Class Containing
The Objects Called Yes Or No.   (Instance-Of Yes (One-Of Yes No)) Is
True, And (Instance-Of Maybe (One-Of Yes No) Is False.  A Common
Use For One-Of Is In Defining Type Restrictions.  For Example, 
The Relation Value-Type Takes A Class As An Argument.  To Specify A
Finite Set Of Possible Values For A Slot, One Can Use
    (Value-Type ?Instance ?Slot (One-Of A B C)).)

(Documentation 
    Subclass-Of
    Class C Is A Subclass Of Parent Class P If And Only If 
Every Instance Of C Is Also An Instance Of P.  A Class May 
Have Multiple Superclasses And Subclasses. Subclass-Of Is Transitive: 
If (Subclass-Of C1 C2) And (Subclass-Of C2 C3) Then (Subclass-Of C1 C3).
   Object-Centered Systems Sometimes Distinguish Between A Subclass-Of
Relationship That Is Asserted And One That Is Inferred.
For Example, (Subclass-Of C1 C3) Might Be Inferred From
Asserting (Subclass-Of C1 C2) And (Subclass-Of C2 C3).
The Functional Interfaces To Such Systems
Might Call The Asserted Form Something Like `Parents' And The Inferred
Form `Ancestors'.  However, Both Are Logically Identical To
Subclass-Of; Distinctions Based On Inference Procedures And The
Current State Of The Knowledge Base Are Not Captured In This
Ontology.)

(Documentation 
    Superclass-Of
    Superclass-Of Is The Inverse Of The Subclass-Of Relation.
It Is Useful To Create An Explicit Inverse Because
There Are Efficient Ways To Assert And Query Superclass And Subclass
Relationships Separately. 
  In Cyc, Superclass-Of Is Called #%Allspecs Because It Is A Slot From
A Collection To All Of Its Specializations (Subclasses).)

(Documentation 
    Subrelation-Of
    A Relation R Is A Subrelation-Of Relation R' If, Viewed As Sets,
R Is A Subset Of R'.  In Other Words, Every Tuple Of R Is Also A Tuple Of
R'.  In Some More Words, If R Holds For Some Arguments Arg_1, Arg_2, ...
Arg_N, Then R' Holds For The Same Arguments.  Thus, A Relation And Its
Subrelation Must Have The Same Arity, Which Could Be Undefined.
  In Cycl, Subrelation-Of Is Called #%Genlslots.)

(Documentation 
    Direct-Instance-Of
    An Individual I Is An Direct-Instance-Of Class C If I Is An
Instance-Of C And There Is No Other Subclass Of C Defined In The
Current Ontology Of Which I Is Also An Instance-Of.  Such A Class C Is
A `Minimal' Or `Most-Specific' Parent Class For The Individual I.  The
Direct Class Is Not Necessarily Unique; An Individual Can Have Several
Most-Specific Classes.  Note That This Relation Is Indexical -- Its
Truth Depends The Contents Of The Current Knowledge Base Rather Than
The World.
  The Distinction Between Instance-Of And Direct-Instance-Of Is _Not_
The Same As The Relationship Between Asserting Instance-Of Directly
And Having The System Infer It.  The Meanings Of Both Instance-Of And
Direct-Instance-Of, And Every Other Object-Level Relation In A
Knowledge Base Mean, Are Independent Of Whether They Are Asserted
Explicitly Or Inferred.
   Cyc Makes The Distinction Between #%Instanceof And #%Allinstanceof.
#%Allinstanceof Means The Same Thing As Instance-Of In Our
Ontology.  However, #%Instanceof Is Subtlely Different From
Direct-Instance-Of.  When Someone Asserts (#%Instanceof I C) To
Cyc, It Means The Same Thing As (#%Allinstanceof I C), But Cyc Creates
A Pointer Between An Instance Unit And A Collection Unit.  Later,
Someone May Define A Subclass C_Sub Of C And Assert (#%Instanceof I
C_Sub), And This Is Consistent With The Earlier #%Instanceof
Assertion.
   Direct-Instance-Of Is Useful For Maintaining A Class Hierarchy
In A Modular, Canonical Form.  It Is Defined Here Because Some Systems
Maintain Direct-Instance-Of And Some Applications Depend On This.)

(Documentation 
    Direct-Subclass-Of
    Direct-Subclass-Of Is The Same Thing As Subclass-Of With An Additional
Constraint: There Is No Other Class `Between' Child And Parent Class In
The Subclass Hierarchy Of The Current Knowledge Base.  In Other Words, If
 (Direct-Subclass-Of C P) Then There Is No Other Defined Class P' In
The Current Knowledge Base That Is A Superclass Of C And Also A
Subclass Of P.
  Note That This Relation Is Indexical -- Its Truth Depends The
Contents Of The Current Knowledge Base Rather Than The World.  There
Certaintly Might Be A Set Of Tuples In The World That Is A Superset Of
C And A Subset Of P, But It Can'T Have Been Defined As A Class In The
Current Knowledge Base If (Direct-Subclass-Of C P) Is True For That
Knowledge Base.
  The Direct-Subclass-Of Of A Class Is Not Necessarily Unique.
  In Systems With Term Classifiers, Direct-Subclass-Of Relations Are
Usually Inferred, Rather Than Asserted.)

(Documentation 
    Arity
    Arity Is The Number Of Arguments That A Relation Can Take.  If A
Relation Can Take An Arbitrary Number Of Arguments, Its Arity Is
Undefined.  For Example, A Function Such As `+' Is Of Undefined Arity;
Its Last Formal Argument Is Specified With A Sequence Variable.  The
Arity Of A Function Is One More Than The Number Of Arguments It Can
Take, In Keeping With The Unified Treatment Of Functions And
Relations.  The Arity Of The Empty Relation (I.E., With No Tuples) Is
Undefined.)

(Documentation 
    Exact-Domain
    The Exact-Domain Of A Relation Is A Relation Whose Tuples (All Of Them)
Are Mapped By The Relation To Instances Of The Range.  A
Binary Relation R Is Defined As A Set Of Tuples Of Form <X,Y>.  If We 
Say (= (Exact-Domain R) D) Then All Of The
X'S Must Be In The Class D, And For Each Instance X Of Class D, The
Relation Maps X To Some Y.  The Exact-Domain Of A Relation Of Arity Other
Than 2 Is The Relation That Represents A Cross Product.  For Example,
The Notation F:A X B -> C, Means That Function F Maps Pairs <A,B> Onto
C'S Where A Is An Instance Of A, B Is An Instance Of B, And C Is An
Instance Of C.  The Exact-Domain Of F Is The Set Of Pairs <A,B> That
Occur In Some Triple <A,B,C> In F.
    Some Treatments Of Functions Define A Function As A _Mapping_ From A
Domain To A Range.  This Ontology Treats Functions As Relations, And 
Relations As Sets Of Tuples.  Thus, Functions And Relations Are _Not_
Defined Relative To Domains And Ranges; The Exact-Domain Is A Function 
Of The Set Of Tuples.  It Follows That All Functions Are `Total' With 
Respect To Their Exact-Domains And `Onto' With Respect To Their Exact-Ranges.
   The Exact-Domain Of A Variable-Arity Relation Is Another Variable-Arity
Relation; The Lengths Of The Tuples In The Exact-Domain Of R Is One Less
Than The Corresponding Tuples In The Relation R.  The Exact-Domain Of A Unary
Relation, Or A Relation That Contains A Tuple Of Length One, Is Undefined.)

(Documentation 
    Exact-Range
    A Relation Maps Elements Of A Domain Onto Element Of A Range. 
For Each Tuple In The Relation, The Last Item Is In The Range, 
And The Tuple Formed By The Preceeding Items Is In The Domain.
The Exact-Range Is The Class Whose Instances Are Exactly Those That 
Appear In The Last Item Of Some Tuple In The Relation.  
  The Exact-Range Of A Relation Is Always A Class, While The 
Exact-Domain May Be A Relation Of Any Arity, Including Variable 
Arity (E.G., The + Function Can Take 0 Or More Arguments, But Its
Exact-Range Is Some Subset Of The Class Number).
  In Kif, Functions Are A Special Case Of Relations.  This
Definition Is Based On Relational Terminology, But Applies To
Functions As Well.  In Discussions Of Functions, One Often Sees The
Notation F:X -> Y.  Usually, X And Y Are Sets Of Elements X And Y.  In
This Ontology, The Unary Function F Is Also A Binary Relation, Where X
Is The Exact-Domain Of F And Y Is The Exact-Range Of F.  This
Generalizes To Cross Products.  For The Function G:A X B X C -> D, The
Domain Is The Ternary Relation Of Tuples (A, B, C) And The Range Is
The Unary Relation Of Tuples (D).  The Exact-Range Of Just Those D'S
That Are Actually The Value Of G On Some (A, B, C).
  The Exact-Range Of A Function Is Unique, And Every Function F 
Maps (Exact-Domain F) _Onto_ (Exact-Range F).  Sometimes The Exact-Range
Of F Is Called The ``Image Of (Exact-Domain F) Under D.''
  The Relation Range Is A _Constraint_ On The Possible Values Of A 
Function.  It Is A Superclass Of The Exact-Range, And Is Not Unique.)

(Documentation 
    Total-On
    A Relation R Is Total-On A Domain Class C If There Are Tuples In The
Relation (X,Y) For Every Instance X Of C.  If The Domain Is A Relation D,
It Represents A Cartesian Product, And The Relation Is Total On D 
If For Every Tuple (X1, X2, ... Xn) In D There Is A Tuple (X1, X2, ... Xn, Y)
In R.)

(Documentation 
    Onto
    A Relation R Is Onto Range Class C Iff For Every Element Y In C There
Is A Tuple In R (X1, X2, ... Y).)

(Documentation 
    Projection
    The Projection Of An N-Ary Relation On Column I Is The Class Whose
Instances Are The Ith Items Of Each Tuple In The Relation.)

(Documentation 
    Composition-Of
    A Binary Relation R Is A Composition-Of A Sequence Of Binary Relations 
R_1, R_2, ... R_N Iff There Exists A Relation R' That Is A Composition-Of
The Sequence R_1 ... R_{N-1}, And R Is The (Composition R_1 R').
  Relations Are Composed Right To Left.  For Example,
If (Composition-Of R (Listof A B C D))
Then R = (Composition D (Composition C (Composition B A))).
  When The Relations Are Unary Functions, The Sequence Corresponds To
Nested Parentheses In Functional Notation.  For Example, If F Is
Composition-Of Functions A, B, And C, (Composition-Of F (Listof A B C))
Means (F ?X) Is Equal To (A (B (C ?X))).)

(Documentation 
    Compose
    Arbitrary-Arity Version Of Composition.  The Left-To-Right
Argument Order Composes Relations Outside-In.  
E.G., (Compose F G H) Means (Composition H (Composition G F)).
If The Relations Are Unary Functions, Then The Composition Order
Corresponds To Nested Function Terms.  For Example, If F,G,H Are Functions,
Then (Value (Compose F G H) ?Arg) Is Equivalent To (F (G (H ?Arg))).)

(Documentation 
    Alias
    Alias Is A Way To Specify That Two Relations Have
The Same Extension.  It Is Logically Equivalent To The =
Relation, Except That It Is Restricted To Relations.)

(Documentation 
    Domain
    Domain Is Short For ``Domain Restriction''.  A Domain Restriction
Of A Binary Relation Is A Constraint On The Exact-Domain Of The
Relation.  A Domain Restriction Is Superclass Of The Exact-Domain;
That Is, All Instances Of The Exact-Domain Of The Relation Are Also
Instances Of The Domain Restriction.  Thus, The Domain Of A Relation 
Is Not Unique.
   In An Ontology, Specifying A Domain Restriction Of A Binary
Relation Is A Way To Specify Partial Information About The Objects 
To Which The Relation Applies.  For Example, One Can State That
Favorite-Beer Is A Relation From Beer Drinkers To Beers As
 (Domain Favorite-Beer Person).  This Says That All People Who Have
A Favorite-Beer Are Instances Of Person, Even Though There May Be Some
Instances Of Person Who Do Not Have A Favorite Beer.
   Representation Systems Can Use These Specifications To Classify Terms And
Check Integrity Constraints.)

(Documentation 
    Domain-Of
    Domain-Of Is The Inverse Of The Domain Relation;
I.E., (Domain-Of D R) Means That D Is A Domain Restriction Of R.  
A Domain-Of A Binary Relation Is A Class To Which The Binary Relation
Can Be Meaningfully Applied; I.E., It Is Possible, But Not Assured,
That There Are Instances D Of D For Which R(D,V) Holds.  Of Course,
Every Instance I For Which R(I,V) Does Hold Is An Instance Of D.
  One Interpretation Of The Assertion (Domain-Of My-Class My-Relation)
Is `The Slot My-Relation May Apply To Some Of The Instances Of
My-Class.' A Less Precise But Common Paraphrase Is `My-Class _Has_ The
Slot My-Relation'.  User Interfaces To Frame And Object Systems Often
Have Some Symbol-Level Heuristic For Showing Slots That `Have' Or `Make
Sense For' The Class.  Keep In Mind That Domain-Of Is A Constraint On
The Logically Consistent Use Of The Relation, Not A Relevance
Assertion.  There Are Many Classes That Are Domains-Of A Given
Relation; Namely, All Superclasses Of The Exact-Domain.  (Thing, For
Example, Is A Domain-Of All Relations.) Therefore, It Is Quite Possible
That Most Of The Instances Of A Domain-Of A Relation Do Not `Make
Sense' For That Relation.
  Whereever One Uses (Domain-Of D R) It Is Equivalent To Adding D To
The List Of Domain Restrictions On The Definition Of R.  In Other Words
If R Was Defined As (Define-Relation R (?X ?Y) :Def (And (A ?X) (B ?Y)))
Then The Statement (Domain-Of D R) Has The Same Meaning As Changing The
Definition To (Define-Relation R (?X ?Y) :Def (And (A ?X) (D ?X) (B ?Y))).
For Modularity Reasons Domain-Of Is Preferred Only When R Is Not Given Its 
Own Definition In An Ontology.)

(Documentation 
    Range
    Range Is Short For ``Range Restriction.''
Specifying A Range Restriction Of A Relation Is A Way To Constrain
The Class Of Objects Which Participate As The Last Argument To The
Relation.  For Any Tuple <D1 D2 ...Dn R> In The Relation, If Class T Is A
Range Restriction Of The Relation, R Must Be An Instance Of T.
    Range Restrictions Are Very Helpful In Maintaining Ontologies.
One Can Think Of A Range Restriction As A Type Constraint On The Value
Of A Function Or Range Of A Relation.  Representation Systems Can Use
These Specifications To Classify Terms And Check Integrity
Constraints.
    If The Restriction On The Range Of The Relation Is Not Captured By
A Named Class, One Can Use Specify The Constraint With A Predicate That 
Defines The Class Implicitly, Coerced Into A Class.  For Example,
  (Kappa (?X) (And (Prime ?X) (< ?X 100)))
Denotes The Class Of Prime Numbers Under 100.
    It Is Consistent To Specify More Than One Range Restriction For A
Relation, As Long As They All Include The Exact-Range Of The Relation.
    Note That Range Restriction Is True Regardless Of What The Restricted
Relation Is Applied To.  For Class-Specific Range Constraints, Use
Slot-Value-Type.)

(Documentation 
    Range-Of
    The Inverse Of Range.  A Class C Is A Range-Of
A Relation R If C Is A Superclass-Of The Exact Range Of R.)

(Documentation 
    Nth-Domain
    Domain Restrictions Generalized To N-Ary Relations.
The Sentence (Nth-Domain Rel 3 Type-Class) Says That
The 3rd Element Of Each Tuple In The Relation Rel Is
An Instance Of Type-Class.)

(Documentation 
    Relation-Universe
    A Relation-Universe Of A Relation Of Any Arity Is A Class
From Which Is Drawn Every Item In Every Tuple Of The Relation.
Like Exact-Domain, It Is Exactly Those Items And No Other.
Thus, To State That The Universe Of A Relation Is Covered By
Some Class, One Can State That The Relation-Universe Is A Subclass
Of The Covering Class.)

(Documentation 
    Has-Value
    Has-Value Is A Way To State That An Instance Has A Value On Some Slot.
Its Third Argument Is A Single Value; One May Use Has-Value Repeatedly
For Each Value Of A Multiple-Valued Relation.
  For Example, (Has-Value I R V_1), (Has-Value I R V_2) Means That
Slot R Applied To Domain Instance I Maps To Values V_1 And V_2.
In Other Words, R(I,V_1) And R(I,V_2) Hold.
   There Is No Closed-World Assumption Implied; There May Be
Other Values For The Specified Slot On A Given Domain Instance.)

(Documentation 
    All-Values
    All-Values Is A Way To State All Of The The Values Of A Slot 
On An Instance. Its Third Argument Is A Set.  If All-Values Are Given
For A Slot On An Instance, There Cannot Be Any Other Values For That 
Slot On That Instance.  For Example, (= (All-Values I R) (Setof V_1 V_2 V_3))
Means That R(I,V_1), R(I,V_2), And R(I,V_3) Hold, And There Is No Other 
Unique V_I For Which R(I,V_I) Holds.)

(Documentation 
    Value-Type
    The Value-Type Of A Binary Relation R With Respect To A Given
Instance D Is A Constraint On The Values Of R When R Is Applied To D.
The Constraint Is Specified As A Class T Such That When R(D,T) Holds, 
T Is An Instance Of T.)

(Documentation 
    Same-Values
    Two Binary Relations R1 And R2 Have The Same-Values On Instance I
If Whenever R1(I,V) Holds For Some Value V, Then R2(I,V) Holds For 
The Same Domain Instance I And Value V.)

(Documentation 
    Value-Cardinality
    The Value-Cardinality Of A Binary-Relation With Respect To A Given
Domain Instance Is The Number Of Range-Elements To Which The Relation
Maps The Domain-Element.  For A Function (Single-Valued Relation), The
Value-Cardinality Is 1 On All Domain Instances For Which The Function
Is Defined.  It Is 0 For Those Instances Outside The Exact Domain Of
The Function.
  Value-Cardinality May Be Used Within The Definition Of A Class To
Specify A Slot Cardinality If Its First Argument Is The Class'S
Instance Variable.)

(Documentation 
    Minimum-Value-Cardinality
    Minimum Value Cardinality Is A Constraint On The Number Of Values To
Which A Binary Relation Can Map A Domain Instance.  It Implies The Existence
Of At Least N Values For A Given Relation On An Instance.)

(Documentation 
    Maximum-Value-Cardinality
    Maximum Value Cardinality Is A Constraint On The Number Of Values To
Which A Binary Relation Can Map A Domain Instance.  It Restrict The Relation
To At Most N Values For A Given A Domain Instance.  A Cardinality Of 0 
Means That The Relation Does Not Hold For That Instance.)

(Documentation 
    Slot-Value-Type
    The Slot-Value-Type Of A Relation R With Respect To A Domain
Class C Is A Constraint On The Values Of R When R Is Applied To
Instances Of C.  The Constraint Is Specified As A Class T Such That
For Any Instance C Of C, When R(C,T), T Is An Instance Of T.)

(Documentation 
    Slot-Cardinality
    If A Slot-Cardinality Of Relation R With Respect To A Domain
Class C Is N, Then For All Instances C Of Class C, R Maps C To Exactly
N Individuals In The Range.  For Single-Valued Relations, The
Slot-Cardinality Is 1.  Specifying A Slot-Cardinality Is A Constraint
Between Classes And Binary-Relations Which Does Not Always Hold; There
Need Not Be Any Fixed Value-Cardinality For R On All Instances Of C.)

(Documentation 
    Minimum-Slot-Cardinality
    Minimum-Value-Cardinality Specifies A Lower Bound On The Number
Of Range Elements To Which A Given Relation Can Map Instance Of A
Given Domain Class.  In Other Words, It Is The Minimum Number Of Slot
Values For A Slot Local To A Class.)

(Documentation 
    Maximum-Slot-Cardinality
    Maximum-Value-Cardinality Specifies An Upper Bound On The Number Of
Range Elements Associated With Any Instance Of A Given Domain Class.
   It Is Inspired By The Classic And Loom `At-Most' Operator.)

(Documentation 
    Single-Valued-Slot
    Single-Valued-Slot Is A Constraint On The Second Argument Of A Binary
Relation That Is Conditional On The First Argument To The Relation Being
An Instance Of A Given Class.  It Is Like Unary-Function, Except It
Is Local To The Values Of The Relation On Instances Of The Given Subset
Of The Domain.)

(Documentation 
    Inherited-Slot-Value
    An Inherited-Slot-Value Of Binary Relation R On Class C Is Value V
For Which R(I,V) Holds On Each Instance I Of C.
There Is No Closed-World Assumption; There May Exist Other Values V_I For Which
R(I,V_I) Holds.  Inherited Values Are Monotonic, Not Default.)

(Documentation 
    All-Inherited-Slot-Values
    The All-Inherited-Slot-Values Of Binary Relation R On Class C Is The Set V
Of Values For Which R(C,S) Holds On Each Instance I Of C And Member V Of V.
Unlike Inherited-Slot-Values, There May Not Exist Any Other Value V_I For Which
R(I,V_I) Holds.  Inherited Values Are Monotonic, Not Default.)

(Documentation 
    Same-Slot-Values
    Let Class C Be In The Domain Of Two Binary Relations R_1 And R_2.
The Relation (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.)

(Documentation 
    Class-Partition
    A Set Of Mutually Disjoint Classes.  Disjointness Of
Classes Is A Special Case Of Disjointness Of Sets.)

(Documentation 
    Subclass-Partition
    A Subclass-Partition Of A Class C Is A Set Of
Subclasses Of C That Are Mutually Disjoint.)

(Documentation 
    Exhaustive-Subclass-Partition
    A Subrelation-Partition Of A Class C Is A Set Of
Mutually-Disjoint Classes (A Subclass Partition) Which Covers C.
Every Instance Of C Is Is An Instance Of Exactly One Of The Subclasses
In The Partition.)

(Documentation Symmetric-Relation
               Relation R Is Symmetric If R(X,Y) Implies R(Y,X).)

(Documentation 
    Antisymmetric-Relation
    Relation R Is An Antisymmetric-Relation If For Distinct X And Y, 
R(X,Y) Implies Not R(Y,X).  In Other Words, For All X,Y,
R(X,Y) And R(Y,X) => X=Y.  R(X,X) Is Still Possible.)

(Documentation 
    Asymmetric-Relation
    A Binary Relation Is Asymmetric If It Is Antisymmetric
And Irreflexive Over Its Exact-Domain.)

(Documentation 
    Reflexive-Relation
    Relation R Is Reflexive If R(X,X) For All X In The Domain Of R.)

(Documentation Irreflexive-Relation
               Relation R Is Irreflexive If If R(A,A) Never Holds.)

(Documentation 
    Transitive-Relation
    Relation R Is Transitive If R(X,Y) And R(Y,Z) Implies R(X,Z).)

(Documentation 
    Weak-Transitive-Relation
    Relation R Is Weak-Transitive If R(X,Y) And R(Y,Z) And X /= Z
Implies R(X,Z).)

(Documentation 
    Equivalence-Relation
    A Relation Is An Equivalence Relation If It Is Reflexive,
Symmetric, And Transitive.)

(Documentation 
    Partial-Order-Relation
    A Relation Is An Partial-Order If It Is Reflexive,
Asymmetric, And Transitive.)

(Documentation 
    Total-Order-Relation
    A Relation R Is An Total-Order If It Is Partial-Order
For Which Either R(X,Y) Or R(Y,X) For Every X Or Y In Its Exact-Domain.)

(=> (Documentation $X $Y) (String $Y))

(Documentation 
    Related-Axioms
    Related-Axioms Is A Relation That Maps Any Object In The Domain Of
Discourse To A Kif Sentence Related To That Object.  Kif Sentences Can
Be Denoted By Quoted Expressions.  The Object Is Not Necessarily A
Symbol.  It Is Usually A Class Or Relation Or Instance Of A Class.
Therefore Related Does Not Mean That The Object Is Mentioned In The
Axiom, And There Is No Syntactic Test For Relatedness.)