types/sorts, roles, etc. in KIF
Tom Gruber <Gruber@Sumex-AIM.Stanford.edu>
Message-id: <2923322200-5068487@KSL-Mac-69>
Date: Thu, 20 Aug 92 10:56:40 PDT
From: Tom Gruber <Gruber@Sumex-AIM.Stanford.edu>
To: interlingua@ISI.EDU
Subject: types/sorts, roles, etc. in KIF
There have been several email messages that talk about KIF including
"sorts" or "types", "concepts", and "roles". For example:
--- Excerpt from John Sowa (Mon, 6 Jul 92 19:49:23 EDT) ---
>> 1. Types. At the KR Advisory Board meeting on March 28, I
>> discussed
>> this point with both Mike and Richard. Mike agreed that it would
>> not cause major theoretical problems to add types or sorts to
>> KIF and that they would be useful in simplifying the mapping to
>> typed languages such as KRSS, conceptual graphs, and most
>> versions of semantic nets and object-oriented languages. But
>> Mike and Richard have not yet made a final decision on adding
>> types to KIF, since there are still some issues that remain to be
>> resolved, especially in the interaction of types with sets and
>> some of the other details of the language. I agree that the
>> interaction of types and sets is a critical issue, and it should
>> have high priority.
--- Excerpt from Robert MacGregor (Tue, 09 Jun 92 09:35:22 PDT) ---
> Also, KIF does not contain anything resembling the frame notion of
> "role". I am curious to know how a role in Ontolingua is translated into
> KIF. Perhaps propositions and roles move us from the realm of KIF to
> ontology?
I thought the Interlingua committee should be aware that there is an
ontology which defines the terminology for extending KIF to accomodate
these kinds of requests. It is called the frame ontology, and is
attached. It demonstrates an important property of KIF as an
interlingua for LOGIC: that it allows one to define more restricted
languages without changing the syntax or semantics of the interlingua.
I claim that a lot of ontological commitments made in the _syntax_ of
existing representation and programming languages can be specified as
a set of definitions of relations, functions, and object constants in
KIF. In the frame ontology, I define a set of concepts sufficient to
translate between KIF and languages such as LOOM, CLASSIC, and KRSS.
KIF has already made ontological commitments to sets of a specific
flavor, sequences, relations as sets of sequences, and functions as
relations. The chapters that describe these commitments can be
thought of as ontologies, since they are just axiomatic definitions
(this is an oversimplification, since some things are included as
operators and some definitions use axiom schemata). Similarly, KIF
includes numbers today, with an implicit ontology left to the reader
(or some interlingua committee member).
I am not arguing that KIF should never include types as a built in
ontology. I am claiming that they could be introduced as extensions
associated with ontologies, rather than as part of the core semantics.
So, consider whether it would be adequate and appropriate to treat
some proposed extensions to the language as proposed ontologies,
albeit very general ones, that simply introduce new terms and define
them axiomatically. I include the frame ontology as an example.
--tom gruber
Note: the following definitions are in Ontolingua syntax, which is
sugar over the KIF definitional forms to accomodate doc strings and
other readability needs. It and pure KIF have been converging and the
differences are minor:
TRANSLATION GUIDE:
define-relation and define-class --> KIF's DEFRELATION
define-function --> KIF's DEFFUNCTION
doc strings ignored in KIF.
:IFF-DEF --> KIF's ":="
:DEF --> KIF's ":=>"
in functions, :LAMBDA-BODY --> KIF's ":="
:CONSTRAINTS --> KIF's "=>" (non definitional implication)
:EQUIVALENT --> KIF's "<=>" (non definitional bi-implication)
:AXIOMS --> KIF's :AXIOM or axioms without a label in a definition
;; -*- Mode:Common-Lisp; Package:ONTOLINGUA; Base:10; Theory:"OL:FRAME-ONTOLOGY" -*-
#|----------------------------------------------------------------------
THE FRAME ONTOLOGY
Version: 2
Last Modified: August 7, 1992
This file contains definitions for the frame ontology. It defines
the terms that capture conventions used in many frame systems
(object-centered knowledge representation systems). Since these
terms are built upon the semantics of KIF, one can think of KIF plus
the frame-ontology as a specialized representation language.
One purpose of this ontology is to enable people using different
representation systems to share ontologies that are organized
along object-centered, term-subsumption lines. Translators of
ontologies written in KIF using the frame ontology, such as those
provided by Ontolingua, allow one to work from a common source
format and yet continue to use existing representation systems.
The definitions in this ontology are based on common usage in the
computer science and mathematics literatures. See the
acknowledgements at the end of the file.
This ontology is specified using the definitional forms provided
by Ontolingua. All of the embedded sentences are in KIF 3.0, and
the whole thing can be translated into pure KIF top level forms
without loss of information.
The basic ontological commitments of this ontology are
- Relations are sets of tuples -- named by predicates
- Functions are a special case of relations
- Classes are unary relations -- no special syntax for types
- "Slots" are not special, just binary relations
- KL-ONE style specs are relations on relations
(second-order relations, not metalinguistic or modal)
----------------------------------------------------------------------
Outline
0. Preliminaries: package and theory definitions
1. Basic categories: relations, classes, functions, sets
2. Basic relationships: subclass, instance, subrelation
3. Basic properties of relations: arity, exact-domain, exact-range
4. Special categories of relations: binary, unary, n-ary, single-valued
5. Special relation relationships: inverse, projection,
composition
6. Restrictions on binary relations: domain, domain-of, range, range-of
7. Special restrictions on relations relative to domains:
value-type, slot-value-type, value-cardinality, slot-cardinality, etc.
8. Organizing classes into mutually-disjoint sets.
class-partition, subclass-partition, exhaustive-subclass-partition
9. Special properties and relations on binary-relations:
symmetry, reflexivity, transitivity
10. Derived properties of binary relations:
equivalence, order, one-to-many, etc.
----------------------------------------------------------------------|#
#|----------------------------------------------------------------------
0. Preliminaries: package and theory definitions
A Note on Packages:
This file has been written "in" the ONTOLINGUA package, which uses
the KIF package. Thus, symbols referenced here that are also exported
>From the KIF package denote the corresponding KIF symbols. It is also the
case that any exported symbols in the KIF package that overlap the native
lisp namespace will have been imported from there into the KIF package
(see the file packages.lisp)
The intent of all this is that users who wish to share
the KIF and Ontolingua vocabulary can enforce a common namespace by
setting up a data package that uses the KIF package. Symbols
interned in this data package that have the same pnames as KIF or
frame-ontology symbols will thus be the same KIF symbols.
----------------------------------------------------------------------|#
(in-package "ONTOLINGUA")
#|----------------------------------------------------------------------
The Frame-Ontology Theory
The definitions in this file use ontolingua forms, and therefore the
ontology exists as a theory called ONTOLINGUA:FRAME-ONTOLOGY. A user's
ontology can include the frame-ontology using the :included-theories
argument of define-theory.
The frame-ontology is a special ontolingua theory. It may be
specialized on implementation types. For instance, there is an
EPIKIT version and a LOOM version of the frame-ontology. To
support the multiple versions, the define-theory form for the
frame ontology is assumed to reside outside of this file. Normal
ontologies might define the theory at the beginning of a file
contrain the definitions.
The following statement only specifies the "current theory" for
this file; it doesn't define the theory.
----------------------------------------------------------------------|#
(in-theory 'FRAME-ONTOLOGY)
#|----------------------------------------------------------------------
1. Basic categories: Relations, Classes, Functions
KIF allows relations of arbitrary and variable arity, defined
as sets of tuples. Classes are unary (one-place) relations.
Functions are relations in which the last item in each tuple is
is the value of the function on the preceding items in the
tuple.
----------------------------------------------------------------------|#
(define-class RELATION (?relation)
"A relation is a set of tuples that represents a relationship among
objects in the universe of discourse. Each tuple is a finite, ordered
sequence (i.e., list) of objects. A relation is also an object
itself, namely, the set of tuples. Tuples are also entities in the
universe of discourse, and can be represented as individual objects,
but they are not equal to their symbol-level representation as lists.
By convention, relations are defined intensionally by specifying
constraints that must hold among objects in each tuple. That is, a
relation is defined by a predicate which holds for sequences of arguments
that are in the relation.
Relations are denoted by relation constants in KIF.
A fact that a particular tuple is a member of a relation is denoted
by (<relation-name> arg_1 arg_2 .. arg_n), where the arg_i are the
objects in the tuple. In the case of binary relations, the fact can
be read as `arg_1 is <relation-name> arg_2' or `a <relation-name> of
arg_1 is arg_2.' The relation constant is a term as well, which
denotes the set of tuples.
"
:iff-def (and (set ?relation)
(forall ?tuple
(=> (member ?tuple ?relation)
(list ?tuple))))
:issues
((:see-also
"In LOOM, relations are called relations."
"In CycL, relations are called relationships."
"In KEE, relations are not supported explicitly."
"In Epikit, relations are called relations."
"In Algernon, relations are called slots.")
("What about slots?"
"Slots can be represented with unary functions, binary relations,
or both. In some systems, all slots are unary functions that
take a frame object as an argument and return a set of objects as
the value of the slot. In other systems, slots are always binary
relations that map frames to individual slot fillers. In the
frame ontology, slots are represented by binary relations, some
of which are also unary functions. A single-valued slot may be
used in the functional position of a KIF term expression. In this
case, the constant naming the relation is a KIF function constant.
In other cases, the constant may be a relation constant or a function
constant.")
("What about variable-arity relations?"
"They are allowed, but need to use a sequence variable in the
definition.")))
(define-class FUNCTION (?relation)
"A function is a mapping from a domain to a range that associates a
domain element with exactly one range element. The elements of the
domain are tuples, as in relations. The range is a class -- a set of
singleton tuples -- and element of the range is an instance of the
class. Functions are also first-class objects in the same sense that
relations are objects: namely, functions can be viewed as sets of
tuples."
:iff-def (and (relation ?relation)
(forall (?tuple1 ?tuple2)
(=> (member ?tuple1 ?relation)
(member ?tuple2 ?relation)
(= (butlast ?tuple1) (butlast ?tuple2))
(= (last ?tuple1) (last ?tuple2)))))
:issues ((:see-also single-valued)))
(define-class CLASS (?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)))
"
:iff-def (and (instance-of ?class relation)
(= (arity ?class) 1))
:issues
((:see-also
"In CycL, classes are called collections."
"In LOOM, classes are called concepts."
"In KEE, classes are called classes."
"In Epikit, classes are not explicitly part of the language but are
conventionally denoted by unary relations, or using a binary
relation such as (ISA <instance> <class>).")))
(define-function THE-CLASS (?set)
"A constructor for referring to the class associated with a set or relation.
Since classes are really sets of single-element tuples (unary relations),
they aren't sets of their instances. This function lets one create the
class whose instances are elements of the set."
:constraints (or (set ?set) (unary-relation ?set))
:lambda-body (cond ((unary-relation ?set)
?set)
((set ?set)
(kappa (?instance) (member ?instance ?set)))))
#|----------------------------------------------------------------------
2. Basic relationships: instance, subclass, subrelation
The basic relationships among classes, functions and other
relations follow from their definitions as sets of tuples and
their semantics as predicates.
----------------------------------------------------------------------|#
(define-relation INSTANCE-OF (?individual ?class)
"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."
:iff-def (and (class ?class)
(holds ?class ?individual))
:equivalent (member (listof ?individual) ?class)
:issues
(("Why not call instance-of `member-of'?"
"Because instance-of is in common usage, and member-of can get confused
with the set and list operators.")
("Why not call instance-of `example-of', or `isa'?" "Because these words
are used to mean many different things in different contexts.")
(:see-also
"In Cyc, instance-of is called #%allInstanceOf."
"In KEE, instance-of is called member.of."
"In LOOM, instance-of is implicit in the syntax (unary predicates)."
"In Epikit, there is no notion of instances, although by convention
people use unary relations to denote instance-of relationships.")
(:see-also direct-instance-of)))
(define-relation SUBCLASS-OF (?child-class ?parent-class)
"One class C is a subclass of parent class P if all of C's instances
are also instances of P. A class may have multiple superclasses and
subclasses. If classes are viewed as sets, subclass-of means subset.
In CycL, subclass-of is called #%allGenls because it is a slot from
a collection to all of its generalizations (superclasses).
In the KL-ONE literature, subclass relationships are also called
subsumption relationships and ISA is sometime used for subclass-of.
Subclass-of is transitive: if (subclass-of C1 C2) and (subclass-of C2 C3)
then (subclass-of C1 C3).
"
:iff-def (and (instance-of ?parent-class class)
(instance-of ?child-class class)
(forall ?instance
(=> (instance-of ?instance ?child-class)
(instance-of ?instance ?parent-class))))
:constraints (transitive subclass-of)
:issues
("It's called Subclass-of instead of subclass or superclass
because the latter are ambiguous about the order of their arguments. We
are following the naming convention that a binary relationship is read
as an english sentence `Domain-element Relation-name Range-value'.
Thus, `person subclass-of animal' rather than `person superclass
animal'."
(:see-also direct-subclass-of)))
(define-relation SUPERCLASS-OF (?parent-class ?child-class)
"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)."
:iff-def (subclass-of ?child-class ?parent-class)
:axioms ((inverse superclass-of subclass-of))
:issues
("We could have named superclass-of something like
`has-subclasses' or `subclasses'. These look better when displayed as
slots on frames. We opted for `superclass-of' because it is less
ambiguous. Frame editors and related tools are free to alias this
relation."))
(define-relation SUBRELATION-OF (?child-relation ?parent-relation)
"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."
:iff-def (and (instance-of ?child-relation relation)
(instance-of ?parent-relation relation)
(forall ?tuple
(=> (member ?tuple ?child-relation)
(member ?tuple ?parent-relation))))
:equivalent (=> (holds ?child-relation @arguments)
(holds ?parent-relation @arguments))
:constraints (=> (defined (arity ?parent-relation))
(= (arity ?child-relation) (arity ?parent-relation)))
:issues (("Do the arities of the relations have to match?"
"No. Used to be defined this way, but it was an
unnecessary restriction. If the parent relation
has a (fixed) arity, then the child's arity must
be equal to it. However, the child could be of
fixed arity and the parent undefined (variable) arity.")))
(define-relation DIRECT-INSTANCE-OF (?individual ?class)
"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."
:def (instance-of ?individual ?class)
:default-constraints ; this generates a default rule
; using KIF's CONSIS operator
(not (exists ?other-class
(and (not (= ?other-class ?class))
(instance-of ?individual ?other-class)
(subclass-of ?other-class ?class))))
:issues
("Some frame-oriented systems organize instance/class relationships in a
way that takes advantage of the direct-instance-of information.
LOOM, for instance, runs a classifier procedure that determines the
direct-instance-of relationship, given some instance-of assertions
and knowledge about the subclass-of relationships among existing
terms."))
(define-relation DIRECT-SUBCLASS-OF (?child-class ?parent-class)
"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."
:def (subclass-of ?child-class ?parent-class)
:default-constraints ; this generates a default rule
; using KIF's CONSIS operator
(not (exists ?other-class
(and (not (= ?other-class ?child-class))
(not (= ?other-class ?parent-class))
(subclass-of ?child-class ?other-class)
(subclass-of ?other-class ?parent-class))))
)
#|----------------------------------------------------------------------
3. Basic properties of relations: arity, exact-domain, exact-range
----------------------------------------------------------------------|#
(define-relation ARITY (?relation ?n)
"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."
:iff-def (and (instance-of ?relation relation)
(not (empty ?relation))
(instance-of ?n integer)
(forall ?tuple
(=> (member ?tuple ?relation)
(= (length ?tuple) ?n))))
:axioms (instance-of ARITY function)
:issues
("KIF 2.2 doesn't _require_ one to declare the arity of a relation,
nor does it require one to use a relation with a consistent number
of arguments. However, relations defined with Ontolingua are always
of fixed arity, which Ontolingua asserts as part of the translation.
This is to facilitate sharing over implemented frame systems, most
of which do not support variable-arity relations."
"Asserting that the arity is undefined is not the same as saying that
the arity is unconstrained. The arity can only exist if the relation
is of fixed arity. Asserting (undefined (arity ?relation)) means
that one _knows_ that the relation has variable arity."))
(define-function EXACT-DOMAIN (?relation)
"The EXACT-DOMAIN of a relation is a relation whose tuples are mapped by
the relation to instances of the range. If we view a binary relation R as a set of
tuples of form <x,y>, then 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 which 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.
It is rare to specify the exact-domain of a relation; typically
restrictions on the domain are specified in ontologies."
:lambda-body (cond ((instance-of ?relation relation)
(setofall (butlast ?tuple)
(member ?tuple ?relation))))
:constraints (instance-of (exact-domain ?relation) relation)
:issues
((:see-also domain)
("Doesn't it have to be a class?" "Only for binary relations.")
"Why require that the complete domain be included; why not allow for
a superset of the true domain? We need to know the exact-domain of a
relation for describing intensional properties such as
reflexivity. Supersets of an exact domain are specified with DOMAIN."))
(define-function EXACT-RANGE (?relation)
"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."
:constraints (and (instance-of ?relation relation)
(instance-of (exact-range ?relation) class))
:lambda-body (the-class (setofall (last ?value)
(member ?tuple ?relation)))
:issues (("Some books define the range of the function as the set Y
in f:X->Y. Why is the range defined as a subset of Y?"
"To unify relations and functions, we conceptualized
functions as sets rather than as mappings (as in category
theory). In the category theory sense, the range
of function f no a property of the function but of a
particular mapping f:X -> Y. This mapping cannot be
specified without its domain and range. In the set
theoretic account of this ontology, the function is
defined extensionally and the range follows.")
(:see-also range)))
#|----------------------------------------------------------------------
4. Special categories of relations: binary, unary, n-ary, single-valued
----------------------------------------------------------------------|#
(define-class N-ARY-RELATION (?relation)
"An N-ary relation is a relation with some FIXED arity."
:iff-def (and (instance-of ?relation relation)
(not (undefined (arity ?relation)))))
(define-class UNARY-RELATION (?relation)
"A unary relation is a relation of arity 1.
Unary relations are the same thing as classes.
In this ontology there is no logical distinction between a
monadic predicate (unary relation) and a type (class)."
:iff-def (and (instance-of ?relation relation)
(= (arity ?relation) 1))
:issues ((:see-also class)))
(define-class BINARY-RELATION (?relation)
"A binary relation maps instances of a class to
instances of another class. Its arity is 2.
Binary relations are often shown as slots in frame systems."
:iff-def (and (instance-of ?relation relation)
(= (arity ?relation) 2)))
(define-class UNARY-FUNCTION (?f)
"A unary function is a functional mapping from instances of a
class to instances of another class. It is a relation of arity 2.
Binary relations are often shown as slots in frame systems."
:iff-def (and (instance-of ?f binary-relation)
(instance-of ?f function)))
(define-relation SINGLE-VALUED (?relation)
"Single-valued relations are binary relations that are functional.
The predicate SINGLE-VALUED is useful for asserting that a slot will
have at most one value without using a function-defining form. It is
restricted to binary relations because it is defined only for slots.
Note that specifying a relation as single valued says that it is
function for _all_ subclasses of its domain."
:iff-def (and (instance-of ?relation binary-relation)
(instance-of ?relation function))
:issues (:see-also locally-single-valued value-cardinality many-to-one))
#|----------------------------------------------------------------------
5. Special relation relationships: inverse, projection,
composition
----------------------------------------------------------------------|#
(define-function INVERSE (?binary-relation)
"One binary relation is the inverse of another if they are
equivalent when their arguments are swapped."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of (inverse ?binary-relation) binary-relation)
(<=> (holds ?binary-relation ?x ?y)
(holds (inverse ?binary-relation) ?y ?x)))
:issues
("Note that INVERSE is a function. It is possible to have more
than one relation constant naming the inverse of a relation, but they
are all = to each other."))
(define-function PROJECTION (?relation ?column)
"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."
:constraints (and (instance-of ?relation n-ary-relation)
(instance-of ?column natural-number)
(=< ?column (arity ?relation))
(instance-of (projection ?relation ?column) class))
:lambda-body (the-class
(setofall ?item
(exists ?tuple
(and (member ?tuple ?relation)
(= (nth ?tuple ?column) ?item))))))
(define-function COMPOSITION (?R1 ?R2)
"The composition of binary relations R_1 and R_2 is a relation R_3
such that R_1(x,y) and R_2(y,z) implies R_3(x,z)."
:result-variable ?R3
:constraints (and (instance-of ?R1 binary-relation)
(instance-of ?R2 binary-relation)
(instance-of ?R3 binary-relation))
:lambda-body (setofall (listof ?x ?z)
(exists ?y
(and (holds ?R1 ?x ?y)
(holds ?R2 ?y ?z)))))
(define-function COMPOSE* (@binary-relations)
"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)))."
:result-variable ?composed-relation
:constraints (and (forall ?R
(=> (item ?R @binary-relations)
(instance-of ?R binary-relation)))
(instance-of ?composed-relation binary-relation))
:lambda-body (cond ((null @binary-relations)
bottom)
((= (length @binary-relations) 1)
(first @binary-relations))
((= (length @binary-relations) 2)
(composition (second @binary-relations)
(first @binary-relations)))
(true
(composition (last @binary-relations)
(value compose*
(butlast @binary-relations))))))
(define-relation ALIAS (?relation-1 ?relation-2)
"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."
:iff-def (and (instance-of ?relation-1 relation)
(instance-of ?relation-2 relation)
(= ?relation-1 ?relation-2))
)
#|----------------------------------------------------------------------
6. Restrictions on relations: domain, range, value-restrictions
----------------------------------------------------------------------|#
(define-relation DOMAIN (?relation ?restriction)
"DOMAIN is short for ``domain restriction''. A domain restriction
of a binary relation is a constraint on the actual domain of the
relation. A domain restriction is superclass of the EXACT-DOMAIN;
that is, all instances of the actual 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."
:iff-def (and (instance-of ?relation binary-relation)
(instance-of ?restriction class)
(subclass-of (exact-domain ?relation) ?restriction))
:issues ((:see-also
"In Cyc, domain is called makesSenseFor.")))
(define-relation DOMAIN-OF (?domain-class ?binary-relation)
"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."
:iff-def (domain ?binary-relation ?domain-class)
:axioms (inverse domain-of domain)
:issues ((:see-also
"In Cyc, domain-of is called canHaveSlots.")))
(define-relation RANGE (?relation ?type)
"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,
(the-class (setofall (?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."
:iff-def (and (instance-of ?relation relation)
(instance-of ?type class)
(subclass-of (exact-range ?relation) ?type))
:issues ((:see-also slot-value-type)))
(define-relation RANGE-OF (?type ?relation)
"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."
:iff-def (range ?relation ?type)
:axioms (inverse range-of range))
#|----------------------------------------------------------------------
7. Special restrictions on relations relative to domains:
value-type, slot-value-type, value-cardinality, slot-cardinality, etc.
In many frame-based systems, there are expressions for describing
constraints on the values or types of slots relative to a class.
Slots are binary relations or unary functions (single-valued
slots). These expressions specify restrictions on slot values
local to a class. For example, within the description of a class,
a slot may be declared to be single valued and its values of some
type. These declarations are only in force when the slot is
applied to instances of the class. Thus, they are not equivalent
to general constraints on binary relations, such as single-valued
and range. The relations below offer primitives for describing
restrictions on binary relations that are relative to particular
domains.
Included in the family of relations defined below are primitives
for handling KL-ONE style concept definitions, in which the
meanings of classes (concepts) can be defined with restrictions on
their slots (roles).
First we will define the relationships between slots and
individual domain instances. These relations might show up in
definitions as constraints on the instances of a class. By
convention the names of these relations refer to ``values''.
The ``lot'' versions will be defined following the ``value''
relations.
----------------------------------------------------------------------|#
(define-relation VALUE-TYPE (?instance ?binary-relation ?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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of ?type class)
(forall ?value
(=> (holds ?binary-relation ?instance ?value)
(instance-of ?value ?type))))
:issues ("VALUE-TYPE is convenient for specifying type restrictions
on slots relative to a class by using the class's instance
variable."
(:see-also SLOT-VALUE-TYPE)))
(define-relation HAS-VALUE (?instance ?binary-relation ?slot-value)
"That is, a relation R HAS-VALUE v on domain instance i when R(i,v) holds.
HAS-VALUE is a way to assert that a slot has a value on a domain instance.
When used in a definition of a class, and the domain-instance argument is
the instance-variable defined for the class, the (HAS-VALUE ?i S v) means
that slot S has the value v on all instances ?i of the class.
There is no closed-world assumption implied; in other words, there many be
other values for the specified slot on a given domain instance."
:iff-def (and (instance-of ?binary-relation binary-relation)
(holds ?binary-relation ?instance ?slot-value))
:issues ("This is for completeness. In definitions, one could
say (slot ?instance value) instead of
(has-value ?instance slot value)."))
(define-relation HAS-VALUES (?instance ?binary-relation ?set-of-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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(forall ?value
(=> (member ?value ?set-of-values)
(has-value ?instance ?binary-relation ?value)))))
(define-relation HAVE-SAME-VALUES (?instance ?slot1 ?slot2)
"Two binary relations R1 and R2 HAVE-SAME-SLOTS if whenever
R1(i,v) holds for some value v, then R2(i,v) holds for the same
domain instance and value."
:iff-def (and (binary-relation ?slot1)
(binary-relation ?slot2)
(<=> (holds ?slot1 ?instance ?value)
(holds ?slot2 ?instance ?value))))
(define-function VALUE-CARDINALITY (?instance ?binary-relation)
"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."
:lambda-body (cardinality (setofall ?y
(holds ?binary-relation ?instance ?y)))
:issues ((:see-also slot-cardinality)))
(define-relation HAS-AT-LEAST (?instance ?binary-relation ?n)
"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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of ?n natural-number)
(>= (value-cardinality ?instance ?binary-relation) ?n))
:issues ((:see-also minimum-slot-cardinality value-cardinality)))
(define-relation HAS-AT-MOST (?instance ?binary-relation ?n)
"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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of ?n natural-number)
(=< 0 (value-cardinality ?instance ?binary-relation ) ?n))
:issues ((:see-also maximum-slot-cardinality value-cardinality)))
(define-relation HAS-ONE (?instance ?binary-relation)
"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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(= (value-cardinality ?instance ?binary-relation) 1)))
(define-relation HAS-SOME (?instance ?binary-relation)
"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."
:iff-def (has-at-least ?instance ?binary-relation 1))
(define-relation CAN-HAVE-ONE (?instance ?binary-relation)
"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."
:iff-def (has-at-most ?instance ?binary-relation 1)
:issues ((:see-also HAS-AT-MOST SINGLE-VALUED-SLOT DOMAIN)))
(define-relation CANNOT-HAVE (?instance ?binary-relation)
"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."
:iff-def (not (instance-of ?instance (exact-domain ?binary-relation))))
(define-relation HAS-VALUE-OF-TYPE (?instance ?binary-relation ?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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of ?type class)
(exists ?slot-value
(holds ?binary-relation ?instance ?slot-value)
(instance-of ?slot-value ?type)))
:issues ((:see-also HAS-SLOT-VALUE-OF-TYPE)))
(define-relation HAS-ONE-OF-TYPE (?instance ?binary-relation ?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."
:iff-def (and (instance-of ?binary-relation binary-relation)
(instance-of ?type class)
(exists ?slot-value
(and (holds ?binary-relation ?instance ?slot-value)
(instance-of ?slot-value ?type)
(forall ?other-value
(=> (holds ?binary-relation ?instance ?other-value)
(= ?other-value ?slot-value))))))
:issues ((:see-also HAS-SINGLE-SLOT-VALUE-OF-TYPE)))
#|----------------------------------------------------------------------
Now we will define the ``slot'' versions of these relations.
These describe relationships between classes and slots, rather
than instances and slots. They are a useful canonical form for
translation into frame systems.
----------------------------------------------------------------------|#
(define-relation SLOT-VALUE-TYPE (?class ?binary-relation ?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."
:iff-def (and (instance-of ?class class)
(instance-of ?binary-relation binary-relation)
(instance-of ?type class)
(forall ?instance
(=> (instance-of ?instance ?class)
(=> (holds ?binary-relation ?instance ?slot-value)
(instance-of ?slot-value ?type)))))
:issues ((:See-also
RANGE
"In LOOM and CLASSIC, slot-value-type is called `ALL'."
"In KEE, slot-value-type is called `VALUECLASS'.")))
(define-relation SLOT-CARDINALITY (?domain-class ?binary-relation ?n)
"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."
:iff-def (=> (instance-of ?instance ?domain-class)
(= (value-cardinality ?instance ?binary-relation) ?n))
:constraints (and (instance-of ?domain-class class)
(instance-of ?binary-relation binary-relation)
(instance-of ?n natural-number))
:axioms (instance-of slot-cardinality function)
:issues ((:see-also
"Specifying that the slot cardinality is = to some integer
is equivalent to using the LOOM and CLASSIC `EXACTLY'
operator.")
("Note that slot-cardinality is a function. That means
that for any domain and relation, there is at most one
integer N that can be the slot-cardinality. If there is
no such fixed number, then the value of the function is
undefined for the given domain and relation.")))
(define-relation MINIMUM-SLOT-CARDINALITY (?domain-class ?relation ?n)
"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."
:iff-def (=> (instance-of ?instance ?domain-class)
(>= (value-cardinality ?instance ?relation) ?n))
:constraints (and (instance-of ?domain-class class)
(instance-of ?relation binary-relation)
(instance-of ?n natural-number))
:issues ((:see-also
"MINIMUM-SLOT-CARDINALITY is inspired by the CLASSIC
and LOOM `AT-LEAST' operator."
"In KEE, MINIMUM-SLOT-CARDINALITY is called
MIN.CARDINALITY.")))
(define-relation MAXIMUM-SLOT-CARDINALITY (?domain-class ?relation ?n)
"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."
:iff-def (=> (instance-of ?instance ?domain-class)
(=< (value-cardinality ?instance ?relation) ?n))
:constraints (and (instance-of ?domain-class class)
(instance-of ?relation binary-relation)
(instance-of ?n natural-number))
:issues ((:see-also
"MAXIMUM-SLOT-CARDINALITY is inspired by the CLASSIC
and LOOM `AT-LEAST' operator."
"In KEE, MAXIMUM-SLOT-CARDINALITY is called
MAX.CARDINALITY.")))
(define-relation SINGLE-VALUED-SLOT (?class ?binary-relation)
"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 single-valued, except it
is local to the values of the relation on instances of the given subset
of the domain."
:iff-def (= (slot-cardinality ?class ?binary-relation) 1)
:equivalent (and (instance-of ?class class)
(instance-of ?binary-relation binary-relation)
(=> (instance-of ?instance1 ?class)
(=> (holds ?binary-relation ?instance ?slot-value1)
(holds ?binary-relation ?instance ?slot-value2)
(= ?slot-value1 ?slot-value2)))))
(define-relation HAS-SLOT-VALUE (?class ?binary-relation ?slot-value)
"A class C HAS-SLOT-VALUE v of relation R if for every instance i
of C, R(i,v)."
:iff-def (and (instance-of ?class class)
(instance-of ?binary-relation binary-relation)
(=> (instance-of ?instance ?class)
(holds ?binary-relation ?class ?slot-value)))
:issues ((:see-also
"HAS-SLOT-VALUE corresponds to LOOM's ``FILLED-BY''
and CLASSIC's ``FILLS''.")))
(define-relation HAS-SLOT-VALUE-OF-TYPE (?domain-class ?relation ?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."
:iff-def (and (instance-of ?domain-class class)
(instance-of ?relation binary-relation)
(instance-of ?type class)
(=> (instance-of ?instance ?domain-class)
(exists ?slot-value
(holds ?relation ?instance ?slot-value)
(instance-of ?slot-value ?range-class))))
:issues ((:see-also
"HAS-VALUE-OF-TYPE corresponds to LOOM's ``SOME'' operator.")))
(define-relation HAS-SINGLE-SLOT-VALUE-OF-TYPE (?class ?binary-relation ?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."
:iff-def (and (instance-of ?class class)
(instance-of ?binary-relation binary-relation)
(instance-of ?type class)
(single-valued-slot ?class ?binary-relation)
(has-slot-value-of-type ?class ?binary-relation ?type))
:issues ((:see-also
"HAS-SINGLE-SLOT-VALUE-OF-TYPE is inspired by LOOM's ``THE'' operator.")))
#|----------------------------------------------------------------------
8. Organizing classes into mutually-disjoint sets.
class-partition, subclass-partition, exhaustive-subclass-partition
The following three relations are used to succinctly state
that classes are mutually disjoint. A partition may be
given a name using define-instance. Alternatively, one
may define a set of subclasses of a given class that are
mutually disjoint. If the set of subclasses covers the
parent class, then the partition is called exhaustive.
These relations are motivated by the partition tags in the
KRSS specification; in KRSS, however, the partitions are not
first-class objects.
----------------------------------------------------------------------|#
(define-class CLASS-PARTITION (?set-of-classes)
"A set of mutually disjoint classes. Disjointness of
classes is a special case of disjointness of sets."
:iff-def (and (set ?set-of-classes)
(forall ?C
(=> (member ?C ?set-of-classes)
(instance-of ?C class)))
(forall (?C1 ?C2)
(=> (and (member ?C1 ?set-of-classes)
(member ?C2 ?set-of-classes)
(not (= ?C1 ?C2)))
(forall (?i)
(=> (instance-of ?i ?C1)
(not (instance-of ?i ?C2)))))))
:issues (("Why not just use the set machinery?"
"We want to localize the relationship between sets
and classes to just a few axioms, so we use the
instance-of machinery here.")))
(define-relation SUBCLASS-PARTITION (?C ?class-partition)
"A subclass-partition of a class C is a set of
subclasses of C that are mutually disjoint."
:iff-def (and (instance-of ?C class)
(instance-of ?class-partition class-partition)
(forall ?subclass
(=> (member ?subclass ?class-partition)
(subclass-of ?subclass ?C)))))
(define-relation EXHAUSTIVE-SUBCLASS-PARTITION (?C ?class-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."
:iff-def (and (subclass-partition ?C ?class-partition)
(forall ?instance
(=> (instance-of ?instance ?C)
(exists ?subclass
(and (member ?subclass ?class-partition)
(member ?instance ?subclass)))))))
(define-relation CAN-BE-ONE-OF (?instance ?set-of-classes)
"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."
:iff-def (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))))))))
(define-relation MUST-BE-ONE-OF (?instance ?set-of-classes)
"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."
:iff-def (and (can-be-one-of ?instance ?set-of-classes)
(exists ?class
(and (member ?class ?set-of-classes)
(instance-of ?instance ?class)))))
#|----------------------------------------------------------------------
9. Special properties and relations on binary-relations:
symmetry, reflexivity, transitivity
----------------------------------------------------------------------|#
(define-relation ASYMMETRIC-RELATION (?R)
"Relation R is asymmetric if it is not symmetric."
:iff-def (and (instance-of ?R binary-relation)
(not (symmetric-relation ?R))))
(define-relation ANTISYMMETRIC-RELATION (?R)
"Relation R is antisymmetric 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."
:iff-def (and (instance-of ?R binary-relation)
(=> (and (holds ?R ?x ?y) (holds ?R ?y ?x))
(= ?x ?y))))
(define-relation ANTIREFLEXIVE-RELATION (?R)
"Relation R is antireflexive if R(a,a) never holds."
:iff-def (and (instance-of ?R binary-relation)
(not (holds ?R ?x ?x))))
(define-relation IRREFLEXIVE-RELATION (?R)
"Relation R is irreflexive if it is not reflexive."
:iff-def (and (instance-of ?R binary-relation)
(not (reflexive ?R))))
(define-relation REFLEXIVE-RELATION (?R)
"Relation R is reflexive if R(x,x) for all x in the domain of R."
:iff-def (and (instance-of ?R binary-relation)
(=> (instance-of ?x (domain ?R))
(holds ?R ?x ?x))))
(define-relation SYMMETRIC-RELATION (?R)
"Relation R is symmetric if R(x,y) implies R(y,x)."
:iff-def (and (instance-of ?R binary-relation)
(=> (holds ?R ?x ?y)
(holds ?R ?y ?x))))
(define-relation TRANSITIVE-RELATION (?R)
"Relation R is transitive if R(x,y) and R(y,z) implies R(x,z)."
:iff-def (and (instance-of ?R binary-relation)
(=> (and (holds ?R ?x ?y) (holds ?R ?y ?z))
(holds ?R ?x ?z))))
(define-relation WEAK-TRANSITIVE-RELATION (?R)
"Relation R is weak-transitive if R(x,y) and R(y,z) and x /= z
implies R(x,z)."
:iff-def (and (instance-of ?R binary-relation)
(=> (and (holds ?R ?x ?y)
(holds ?R ?y ?z)
(not (= ?x ?z)))
(holds ?R ?x ?z))))
#|----------------------------------------------------------------------
10. Derived properties of binary relations:
equivalence, order, etc.
----------------------------------------------------------------------|#
(define-relation EQUIVALENCE-RELATION (?R)
"A relation is an equivalence relation if it is reflexive,
symmetric, and transitive."
:iff-def (and (reflexive-relation ?R)
(symmetric-relation ?R)
(transitive-relation ?R)))
(define-relation PARTIAL-ORDER-RELATION (?R)
"A relation is an partial-order if it is reflexive,
antisymmetric, and transitive."
:iff-def (and (reflexive-relation ?R)
(antisymmetric-relation ?R)
(transitive-relation ?R)))
(define-relation TOTAL-ORDER-RELATION (?R)
"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 domain."
:iff-def (and (partial-order ?R)
(=> (and (instance-of ?x (domain ?R))
(instance-of ?y (domain ?R)))
(or (holds ?R ?x ?y)
(holds ?R ?y ?x)))))
#|----------------------------------------------------------------------
ACKNOWLEDGEMENTS
The definitions in this ontology are based on common usage in the
computer science and mathematics literatures. Some of the
terminology of functions and relations is based on the book Naive
Set Theory, by Paul Halmos (Princeton, NJ: D. Van Nostrand,
1960). Reed Letsinger of Hewlett-Packard and Stanford University
proposed the uniform treatment of relations and functions as sets
of tuples, and wrote many of the definitions of second-order
relations. The CYC system (Doug Lenat and R. V. Guha, 1990) was
an inspiration for the utility of many of the distinctions
included. The KRSS specification for terminological languages
(Bob MacGregor, Peter Patel-Schneider, and Bill Swartout) was the
source and motivation for several primitives. Richard Fikes and
Mike Genesereth lead the effort to a specification for KIF that is
clear and expressive enough to be a solid foundation for this and
future ontologies. Fritz Mueller made many useful comments and
suggestions, and implemented code to translate from these
primitives into existing representation systems.
----------------------------------------------------------------------|#