I am trying to program an Intelligent Agent using JESS as my programming environment and as my inference engine. One of my requirements is to draw in the Domain's rule base from an ontology.
My ontology was done with Stanford's Ontolingua. Ontolingua will translate an ontology to CLIPS and provides it as a .gf file; my translated ontology is attached (can be opened with a text editor).
Mr. Friedman_Hill replied:
>Unfortunately ontolingua is using "COOL," the CLIPS Object-Oriented >Language, which is not supported by Jess. Instead of using the COOL >object system, Jess uses Java objects. There's no direct way to make >the translation you want to make: you'd have to understand what >Ontolingua was trying to do and recode in Jess. If you understood what >Ontolingua wanted to do, you could almost certainly write a program to >translate your ontology directly into Jess instead.
I am trying to figure out how to input this data into JESS. Does anyone have any experience? Is there any example code that I can look at to help me? I will happily acknowledge any help I receive. My other option as I see it is to redo my ontology in Protege.Mr. Friedman_Hill replied:
>Go ahead and ask on the Jess list if anyone's done this already, or >knows of any alternatives.
Sincerely, Mike Johnson Major, U.S. Army & Virginia Tech Grad Student H:(703) 658-8671 W:(703) 706-1291 (DSN 235)Get more from the Web. FREE MSN Explorer download : http://explorer.msn.com
;;; Translation of #<Ontology Cs6804_Project1_Ms_Cs_Ontology 13C09E06>
;;; into target language Clips
;;; WARNING: The ontology being defined in this file,
Cs6804_Project1_Ms_Cs_Ontology,
;;; depends on the following included ontologies:
;;; Frame-Ontology.
;;; Since this file was generated in standalone mode,
;;; (i.e., *clips-standalone-mode* was true),
;;; these modules are not included and stub definitions of
;;; essential classes will be defined below.
(defmodule Cs6804_Project1_Ms_Cs_Ontology "<UL><LI>The objective of this
ontology is to define the requirements for attaining the Virginia Tech
Computer Science Department's Masters degree in Computer Science.
<LI>The purpose of this ontology is to make the registration process easier
for CS students."
(export ?ALL))
;;; Translation of definitions in included ontology Kif-Extensions
;;; into target language Clips
(defclass Thing "This is only a stubbed definition."
(is-a INITIAL-OBJECT)
(slot OTHER-AXIOMS
(create-accessor read-write))
(slot DOCUMENTATION
(create-accessor read-write))
)
(defclass Undefined "True of terms denoting the bottom object,
usually meaning that a function is undefined
on given arguments. There is exactly one
object in the universe of discourse that is
undefined, called BOTTOM. Functional terms that
are undefined are equal to this special element.
<H3>Notes:</H3>
<UL>UNDEFINED is not in the KIF 3.0 spec, but is implicitly there.</UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Undefined ?Value) (= ?Value Bottom))
(=> (= ?Value Bottom) (Undefined ?Value))
(<= (Undefined ?Value) (= ?Value Bottom))
(Template-Slot-Value = Undefined Bottom)
(<=> (Undefined ?Value) (= ?Value Bottom))
(Nth-Argument-Name Undefined 1 '?Value)
(Slot-Of Instance-Of Bottom))")
(create-accessor read-write))
)
(defclass Defined "A term is defined if it does not denote the undefined
object,
called bottom. (defined (F x)) means that the function F is
defined for the object x. (F x) denotes its value. In relational
terminology, (defined (F x)) means (exists ?y (F x ?y)).
<H3>Notes:</H3>
<UL>DEFINED is not in the KIF 3.0 spec.</UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Defined ?X) (Not (Undefined ?X)))
(=> (Not (Undefined ?X)) (Defined ?X))
(<= (Defined ?X) (Not (Undefined ?X)))
(<=> (Defined ?X) (Not (Undefined ?X)))
(Nth-Argument-Name Defined 1 '?X))")
(create-accessor read-write))
)
(defclass Relation "This is only a stubbed definition."
(is-a Thing)
(slot Alias
(create-accessor read-write))
(slot Documentation
(create-accessor read-write))
(slot Domain
(create-accessor read-write))
(slot Onto
(create-accessor read-write))
(slot Range
(create-accessor read-write))
(slot Related-Axioms
(create-accessor read-write))
(slot Subrelation-Of
(create-accessor read-write))
(slot Has-Subrelation
(create-accessor read-write))
(slot Total-On
(create-accessor read-write))
(slot Arity
(create-accessor read-write))
(slot Function-Arity
(create-accessor read-write))
(slot Exact-Domain
(create-accessor read-write))
(slot Exact-Range
(create-accessor read-write))
(slot Relation-Universe
(create-accessor read-write))
)
(defclass Function "This is only a stubbed definition."
(is-a RELATION)
)
(make-instance [Set-Cardinality] of Function
(Arity 2)
(Function-Arity 1)
(Range Integer)
(Domain Set)
(Documentation "Returns the number of elements in a set.
<H3>Notes:</H3>
<UL>not explicitly defined in the KIF 3.0 spec</UL>")
(OTHER-AXIOMS "((=> (= (Set-Cardinality ?Set) ?Integer)
(And
(Exists (@Elements)
(And (= ?Set (Setof @Elements))
(= ?Integer (Length (Listof @Elements)))))
(Set ?Set)))
(=>
(And
(Exists (@Elements)
(And (= ?Set (Setof @Elements))
(= ?Integer (Length (Listof @Elements)))))
(Set ?Set))
(= (Set-Cardinality ?Set) ?Integer))
(<= (= (Set-Cardinality ?Set) ?Integer)
(And
(Exists (@Elements)
(And (= ?Set (Setof @Elements))
(= ?Integer (Length (Listof @Elements)))))
(Set ?Set)))
(<=> (= (Set-Cardinality ?Set) ?Integer)
(And
(Exists (@Elements)
(And (= ?Set (Setof @Elements))
(= ?Integer (Length (Listof @Elements)))))
(Set ?Set)))
(=> (= (Set-Cardinality ?Set) ?Integer) (Set ?Set))
(=> (= (Set-Cardinality ?Set) ?Integer)
(Exists (@Elements)
(And (= ?Set (Setof @Elements))
(= ?Integer (Length (Listof @Elements))))))
(Nth-Argument-Name Set-Cardinality 1 '?Set))")
)
;;; Forward declaration for external reference Set.
;;; Forward declaration for Set.
(loom:defconcept Set :only-if-no-preexisting-definition-p common-lisp:t)
(defclass Finite-Set "A set that has only finite elements
<H3>Notes:</H3>
<UL>not explicitly defined in the KIF 3.0 spec</UL>"
(is-a Set)
(slot OTHER-AXIOMS
(default "((=> (Finite-Set ?F-Set)
(And (Exists (@Elements) (= ?F-Set (Setof @Elements)))
(Set ?F-Set)))
(=>
(And (Exists (@Elements) (= ?F-Set (Setof @Elements)))
(Set ?F-Set))
(Finite-Set ?F-Set))
(<= (Finite-Set ?F-Set)
(And (Exists (@Elements) (= ?F-Set (Setof @Elements)))
(Set ?F-Set)))
(<=> (Finite-Set ?F-Set)
(And (Exists (@Elements) (= ?F-Set (Setof @Elements)))
(Set ?F-Set)))
(=> (Finite-Set ?F-Set)
(Exists (@Elements) (= ?F-Set (Setof @Elements))))
(=> (Finite-Set ?F-Set) (Set ?F-Set))
(Nth-Argument-Name Finite-Set 1 '?F-Set))")
(create-accessor read-write))
)
(make-instance [Identity] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The value of the identity function is just its
argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Identity 1 '?X))")
)
(defclass Positive-Integer "An integer greater than zero, not including
zero.
A less ambiguous name for KIF's NATURAL."
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((=> (Positive-Integer ?X) (And (> ?X 0) (Integer ?X)))
(=> (And (> ?X 0) (Integer ?X)) (Positive-Integer ?X))
(<= (Positive-Integer ?X) (And (> ?X 0) (Integer ?X)))
(<=> (Positive-Integer ?X) (And (> ?X 0) (Integer ?X)))
(=> (Positive-Integer ?X) (> ?X 0))
(=> (Positive-Integer ?X) (Integer ?X))
(Nth-Argument-Name Positive-Integer 1 '?X))")
(create-accessor read-write))
)
(defclass Non-Negative-Integer "An integer greater than or equal to zero."
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((=> (Non-Negative-Integer ?X) (And (>= ?X 0) (Integer ?X)))
(=> (And (>= ?X 0) (Integer ?X)) (Non-Negative-Integer ?X))
(<= (Non-Negative-Integer ?X) (And (>= ?X 0) (Integer ?X)))
(<=> (Non-Negative-Integer ?X) (And (>= ?X 0) (Integer ?X)))
(=> (Non-Negative-Integer ?X) (>= ?X 0))
(=> (Non-Negative-Integer ?X) (Integer ?X))
(Nth-Argument-Name Non-Negative-Integer 1 '?X))")
(create-accessor read-write))
)
;;; Forward declaration for external reference List.
;;; --- In the definition of Class STRING
;;;
;;; Not translating List because it is already directly
;;; supported by LOOM.
(defclass String "A string is a sequence of characters.
<H3>Notes:</H3>
<UL>STRING is not in the KIF 3.0 spec!</UL>"
(is-a List)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name String 1 '?S))")
(create-accessor read-write))
)
(defclass Vector "A vector is a sequence of values. This is reified in the
implementation
as a vector object.
<H3>Notes:</H3>
<UL>STRING is not in the KIF 3.0 spec!</UL>"
(is-a List)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Vector 1 '?S))")
(create-accessor read-write))
)
;;; Forward declaration for external reference Individual.
;;; Forward declaration for |OL-USER::INDIVIDUAL|.
(loom:defconcept |OL-USER::INDIVIDUAL| :only-if-no-preexisting-definition-p
common-lisp:t)
(defclass Symbol "A symbol is a syntactic entity. It is used
as a nominal identifier. Unlike a STRING, the
sequence of characters that spell the symbol are
not an intrinsic property.
<H3>Notes:</H3>
<UL>SYMBOL is not in the KIF 3.0 spec!<B>See-Also: </B>word</UL>"
(is-a Individual)
(slot OTHER-AXIOMS
(default "((=> (Symbol ?X) (Not (List ?X)))
(Nth-Argument-Name Symbol 1 '?X))")
(create-accessor read-write))
)
(make-instance [List-To-Set] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "denotes the set consisting of the elements of the list.
Essentially removes duplicates and order information from the list.")
(OTHER-AXIOMS "((Nth-Argument-Name List-To-Set 1 '?List))")
)
(make-instance [Second-Item] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "returns the second item in the specified list.
If the length of the list is 0 or 1, this function
is undefined. This is different from Lisp's SECOND function,
which returns NIL, which means both false and null list.")
(OTHER-AXIOMS "((Nth-Argument-Name Second-Item 1 '?List))")
)
;;; Translation of definitions in included ontology Frame-Ontology
;;; into target language Clips
(defclass 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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>In Loom, relations are called relations.
<BR>In CycL, relations are called relationships.
<BR>In KEE, relations are not supported explicitly.
<BR>In Epikit, relations are called relations.
<BR>In Algernon, relations are called slots.
<BR>What about slots?
<BR>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.
<BR>What about variable-arity relations?
<BR>They are allowed, but need to use a sequence variable in the
definition.
<BR>Originally defined in the KIF-RELATIONS ontology</UL>
<H3>Notes:</H3>
<UL>Functions and relations are defined in the frame ontology.
Inserted here for completeness.</UL>
"
(is-a Thing)
(slot Alias
(create-accessor read-write))
(slot Documentation
(create-accessor read-write))
(slot Domain
(create-accessor read-write))
(slot Onto
(create-accessor read-write))
(slot Range
(create-accessor read-write))
(slot Related-Axioms
(create-accessor read-write))
(slot Subrelation-Of
(create-accessor read-write))
(slot Has-Subrelation
(create-accessor read-write))
(slot Total-On
(create-accessor read-write))
(slot Arity
(create-accessor read-write))
(slot Function-Arity
(create-accessor read-write))
(slot Exact-Domain
(create-accessor read-write))
(slot Exact-Range
(create-accessor read-write))
(slot Relation-Universe
(create-accessor read-write))
(slot OTHER-AXIOMS
(default "((=> (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(=>
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation))
(Relation ?Relation))
(<= (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(<=> (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(=> (Relation ?Relation)
(=> (Member ?Tuple ?Relation) (List ?Tuple)))
(=> (Relation ?Relation) (Set ?Relation))
(Nth-Argument-Name Relation 1 '?Relation)
(=> (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(=> (And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set
?R))
(Relation ?R))
(<= (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(<=> (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(=> (Relation ?R) (Forall (?X) (=> (Member ?X ?R) (List
?X))))
(=> (Relation ?R) (Set ?R)) (Nth-Argument-Name Relation 1
'?R))")
(create-accessor read-write))
(multislot Subrelation-Of
(create-accessor read-write)
(type INSTANCE))
(single-slot Arity
(create-accessor read-write)
(type Integer))
(single-slot Exact-Domain
(create-accessor read-write)
(type INSTANCE))
(single-slot Exact-Range
(create-accessor read-write)
(type INSTANCE))
(multislot Alias
(create-accessor read-write)
(type INSTANCE))
(single-slot Range-Name
(create-accessor read-write)
(type INSTANCE))
(multislot Range-Subclass-Of
(create-accessor read-write)
(type INSTANCE))
(single-slot Relation-Universe
(create-accessor read-write)
(type INSTANCE))
)
(defclass Class "An augmentation of CLASS in the frame-ontology to make the
frame-ontology
be more self-consistent when OKBC's kb-local-only-p is true.
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-ontologetic
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)
:iff-def (member ?color (setof red green blue)))
<H3>Notes:</H3>
<UL><B>See-Also: </B>In CycL, classes are called collections.
<BR>In Loom, classes are called concepts.
<BR>In KEE, classes are called classes.
<BR>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>).
<BR></UL>
"
(is-a Relation Thing)
(slot OTHER-AXIOMS
(default "((=> (Class ?Class) (And (= (Arity ?Class) 1) (Relation
?Class)))
(=> (And (= (Arity ?Class) 1) (Relation ?Class)) (Class
?Class))
(<= (Class ?Class) (And (= (Arity ?Class) 1) (Relation
?Class)))
(<=> (Class ?Class)
(And (= (Arity ?Class) 1) (Relation ?Class)))
(=> (Class ?Class) (Relation ?Class))
(Nth-Argument-Name Class 1 '?Class))")
(create-accessor read-write))
(single-slot Arity
(create-accessor read-write)
(default (1))
(type Integer))
(single-slot All-Instances
(create-accessor read-write)
(type INSTANCE))
(multislot Exhaustive-Decomposition
(create-accessor read-write))
(multislot Disjoint-Decomposition
(create-accessor read-write)
(type INSTANCE))
)
(defclass Named-Axiom "The class of all named axioms."
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Named-Axiom 1 '?Axiom))")
(create-accessor read-write))
)
(defclass Function "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.
<H3>Notes:</H3>
<UL>Originally defined in the KIF-RELATIONS ontology</UL>
<H3>Notes:</H3>
<UL>Functions and relations are defined in the frame ontology.
Inserted here for completeness.</UL>
"
(is-a RELATION)
(slot OTHER-AXIOMS
(default "((=> (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(=>
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation))
(Function ?Relation))
(<= (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(<=> (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(=> (Function ?Relation)
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2))))
(=> (Function ?Relation) (Relation ?Relation))
(Nth-Argument-Name Function 1 '?Relation)
(=> (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(=>
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F))
(Function ?F))
(<= (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(<=> (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(=> (Function ?F)
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M)))))
(=> (Function ?F) (Relation ?F))
(Nth-Argument-Name Function 1 '?F))")
(create-accessor read-write))
(single-slot Function-Arity
(create-accessor read-write)
(type Integer))
)
;;; --- In the definition of Class INDIVIDUAL-THING
;;;
;;; Thing has not been included in the superset list
;;; of Individual-Thing because Thing
;;; is already a superclass of Individual.
;;;
(defclass 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)."
(is-a Individual)
(slot OTHER-AXIOMS
(default "((=> (Individual-Thing ?X) (And (Individual ?X) (Thing ?X)))
(=> (And (Individual ?X) (Thing ?X)) (Individual-Thing ?X))
(<= (Individual-Thing ?X) (And (Individual ?X) (Thing ?X)))
(<=> (Individual-Thing ?X) (And (Individual ?X) (Thing ?X)))
(=> (Individual-Thing ?X) (Individual ?X))
(=> (Individual-Thing ?X) (Thing ?X))
(Nth-Argument-Name Individual-Thing 1 '?X))")
(create-accessor read-write))
)
(make-instance [Subdefinition-Of] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The ?child is a subdefinition-of the ?parent. Many
languages allow
subdefinitions within the lexical scope of a parent definition. For
example: Lisp (labels, flet), C (type definitions), Pascal, IDL.")
(OTHER-AXIOMS "((Nth-Argument-Name Subdefinition-Of 1 '?Child))")
)
(make-instance [Has-Subdefinition] of Relation
(Arity 2)
(Documentation "The ?parent may have several subdefinitions, one of
which is child.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Subdefinition 2 '?Child)
(Nth-Argument-Name Has-Subdefinition 1 '?Parent))")
)
(make-instance [All-Instances] of Function
(Arity 2)
(Function-Arity 1)
(Range Set)
(Domain Class)
(Documentation "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.
<H3>Notes:</H3>
<UL>Is all-instances the inverse of instance-of?
<BR>No. Instance-of maps individual instances to classes,
whereas all-instances maps classes to sets of instances.
<BR>The name all-instances is borrowed from Cyc.<B>Example:
</B>(all-instances truth-values (setof true false))
<BR></UL>")
(OTHER-AXIOMS "((=> (= (All-Instances ?Class) ?Set-Of-Instances)
(And
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class)))
(Set ?Set-Of-Instances) (Class ?Class)))
(=>
(And
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class)))
(Set ?Set-Of-Instances) (Class ?Class))
(= (All-Instances ?Class) ?Set-Of-Instances))
(<= (= (All-Instances ?Class) ?Set-Of-Instances)
(And
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class)))
(Set ?Set-Of-Instances) (Class ?Class)))
(<=> (= (All-Instances ?Class) ?Set-Of-Instances)
(And
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class)))
(Set ?Set-Of-Instances) (Class ?Class)))
(=> (= (All-Instances ?Class) ?Set-Of-Instances)
(Class ?Class))
(=> (= (All-Instances ?Class) ?Set-Of-Instances)
(Set ?Set-Of-Instances))
(=> (= (All-Instances ?Class) ?Set-Of-Instances)
(Forall (?Instance)
(<=> (Member ?Instance ?Set-Of-Instances)
(Instance-Of ?Instance ?Class))))
(Nth-Argument-Name All-Instances 1 '?Class))")
)
(make-instance [Subrelation-Of] of Relation
(Arity 2)
(Range Relation)
(Domain Relation)
(Documentation "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.
<H3>Notes:</H3>
<UL>Do the arities of the relations have to match?
<BR>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.
<BR></UL>")
(OTHER-AXIOMS "((=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Child-Relation)
(Member ?Tuple ?Parent-Relation)))
(Relation ?Parent-Relation) (Relation ?Child-Relation)))
(=>
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Child-Relation)
(Member ?Tuple ?Parent-Relation)))
(Relation ?Parent-Relation) (Relation ?Child-Relation))
(Subrelation-Of ?Child-Relation ?Parent-Relation))
(<= (Subrelation-Of ?Child-Relation ?Parent-Relation)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Child-Relation)
(Member ?Tuple ?Parent-Relation)))
(Relation ?Parent-Relation) (Relation ?Child-Relation)))
(<=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
(=> (Holds ?Child-Relation @Arguments)
(Holds ?Parent-Relation @Arguments)))
(<=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Child-Relation)
(Member ?Tuple ?Parent-Relation)))
(Relation ?Parent-Relation) (Relation ?Child-Relation)))
(=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
(Forall (?Tuple)
(=> (Member ?Tuple ?Child-Relation)
(Member ?Tuple ?Parent-Relation))))
(Relation ?Parent-Relation) (Relation ?Child-Relation)
(=> (Subrelation-Of ?Child-Relation ?Parent-Relation)
(=> (Defined (Arity ?Parent-Relation))
(= (Arity ?Child-Relation) (Arity ?Parent-Relation))))
(Nth-Argument-Name Subrelation-Of 2 '?Parent-Relation)
(Nth-Argument-Name Subrelation-Of 1 '?Child-Relation))")
)
(make-instance [Has-Subrelation] of Relation
(Arity 2)
(Documentation "The inverse relation for SubRelation-Of.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Subrelation 2 '?R2)
(Nth-Argument-Name Has-Subrelation 1 '?R1))")
)
(make-instance [Arity] of Function
(Arity 2)
(Function-Arity 1)
(Range Integer)
(Domain Relation)
(Documentation "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.
<H3>Notes:</H3>
<UL>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.</UL>")
(OTHER-AXIOMS "((=> (= (Arity ?Relation) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N)))
(Integer ?N) (Not (Empty ?Relation)) (Relation
?Relation)))
(=>
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N)))
(Integer ?N) (Not (Empty ?Relation)) (Relation
?Relation))
(= (Arity ?Relation) ?N))
(<= (= (Arity ?Relation) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N)))
(Integer ?N) (Not (Empty ?Relation)) (Relation
?Relation)))
(<=> (= (Arity ?Relation) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N)))
(Integer ?N) (Not (Empty ?Relation)) (Relation
?Relation)))
(=> (= (Arity ?Relation) ?N) (Relation ?Relation))
(=> (= (Arity ?Relation) ?N) (Not (Empty ?Relation)))
(=> (= (Arity ?Relation) ?N) (Integer ?N))
(=> (= (Arity ?Relation) ?N)
(Forall (?Tuple)
(=> (Member ?Tuple ?Relation) (= (Length ?Tuple) ?N))))
(Nth-Argument-Name Arity 1 '?Relation))")
)
(make-instance [Function-Arity] of Function
(Arity 2)
(Function-Arity 1)
(Range Integer)
(Domain Function)
(Documentation "Arity is the number of arguments that a function can
take. If a
function 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
RELATION-ARITY of a function is one more than the FUNCTION-ARITY, i.e., the
number of arguments it can take. The arity of the empty function
(i.e., with no tuples) is undefined.")
(OTHER-AXIOMS "((=> (= (Function-Arity ?Function) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Function)
(= (Length ?Tuple) (+ 1 ?N))))
(Integer ?N) (Not (Empty ?Function)) (Function
?Function)))
(=>
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Function)
(= (Length ?Tuple) (+ 1 ?N))))
(Integer ?N) (Not (Empty ?Function)) (Function
?Function))
(= (Function-Arity ?Function) ?N))
(<= (= (Function-Arity ?Function) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Function)
(= (Length ?Tuple) (+ 1 ?N))))
(Integer ?N) (Not (Empty ?Function)) (Function
?Function)))
(<=> (= (Function-Arity ?Function) ?N)
(And
(Forall (?Tuple)
(=> (Member ?Tuple ?Function)
(= (Length ?Tuple) (+ 1 ?N))))
(Integer ?N) (Not (Empty ?Function)) (Function
?Function)))
(=> (= (Function-Arity ?Function) ?N) (Function
?Function))
(=> (= (Function-Arity ?Function) ?N)
(Not (Empty ?Function)))
(=> (= (Function-Arity ?Function) ?N) (Integer ?N))
(=> (= (Function-Arity ?Function) ?N)
(Forall (?Tuple)
(=> (Member ?Tuple ?Function)
(= (Length ?Tuple) (+ 1 ?N)))))
(=> (= (Function-Arity ?F) ?A)
(And (Function ?F) (= (Arity ?F) (+ 1 ?A))))
(Nth-Argument-Name Function-Arity 1 '?Function))")
)
(make-instance [Exact-Domain] of Function
(Arity 2)
(Function-Arity 1)
(Range Relation)
(Domain Relation)
(Documentation "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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>domainexact-rangeDoesn't it have to be a class?
<BR>Only for binary relations.
<BR>Why require that the complete domain be included; why not allow for
a superset of the true domain?
<BR>We need to know the exact-domain of a relation for describing
properties such as reflexivity. Supersets of an exact
domain are specified with DOMAIN.
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(And
(<=> (Member ?But-Last-Of-Tuple ?Domain-Relation)
(And (Member ?Tuple ?Relation)
(= ?But-Last-Of-Tuple (Butlast ?Tuple))))
(=> (Member ?Tuple ?Relation)
(Not (Empty (Butlast ?Tuple))))
(Relation ?Domain-Relation) (Relation ?Relation)))
(=>
(And
(<=> (Member ?But-Last-Of-Tuple ?Domain-Relation)
(And (Member ?Tuple ?Relation)
(= ?But-Last-Of-Tuple (Butlast ?Tuple))))
(=> (Member ?Tuple ?Relation)
(Not (Empty (Butlast ?Tuple))))
(Relation ?Domain-Relation) (Relation ?Relation))
(= (Exact-Domain ?Relation) ?Domain-Relation))
(<= (= (Exact-Domain ?Relation) ?Domain-Relation)
(And
(<=> (Member ?But-Last-Of-Tuple ?Domain-Relation)
(And (Member ?Tuple ?Relation)
(= ?But-Last-Of-Tuple (Butlast ?Tuple))))
(=> (Member ?Tuple ?Relation)
(Not (Empty (Butlast ?Tuple))))
(Relation ?Domain-Relation) (Relation ?Relation)))
(<=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(And
(<=> (Member ?But-Last-Of-Tuple ?Domain-Relation)
(And (Member ?Tuple ?Relation)
(= ?But-Last-Of-Tuple (Butlast ?Tuple))))
(=> (Member ?Tuple ?Relation)
(Not (Empty (Butlast ?Tuple))))
(Relation ?Domain-Relation) (Relation ?Relation)))
(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(Relation ?Relation))
(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(Relation ?Domain-Relation))
(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(=> (Member ?Tuple ?Relation)
(Not (Empty (Butlast ?Tuple)))))
(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
(<=> (Member ?But-Last-Of-Tuple ?Domain-Relation)
(And (Member ?Tuple ?Relation)
(= ?But-Last-Of-Tuple (Butlast ?Tuple)))))
(Nth-Argument-Name Exact-Domain 1 '?Relation))")
)
(make-instance [Exact-Range] of Function
(Arity 2)
(Function-Arity 1)
(Range Class)
(Domain Relation)
(Documentation "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 preceding 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.
<H3>Notes:</H3>
<UL>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?
<BR>To unify relations and functions, we conceptualized
functions as sets rather than as mappings (as in category
ontology). In the category ontology sense, the range
of function f is not 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
ontologetic account of this ontology, the function is
defined extensionally and the range follows.
<BR><B>See-Also: </B>rangeexact-domain</UL>")
(OTHER-AXIOMS "((=> (= (Exact-Range ?Relation) ?Range-Class)
(And
(<=> (Holds ?Range-Class ?Range-Instance)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Last ?Tuple) ?Range-Instance))))
(Class ?Range-Class) (Relation ?Relation)))
(=>
(And
(<=> (Holds ?Range-Class ?Range-Instance)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Last ?Tuple) ?Range-Instance))))
(Class ?Range-Class) (Relation ?Relation))
(= (Exact-Range ?Relation) ?Range-Class))
(<= (= (Exact-Range ?Relation) ?Range-Class)
(And
(<=> (Holds ?Range-Class ?Range-Instance)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Last ?Tuple) ?Range-Instance))))
(Class ?Range-Class) (Relation ?Relation)))
(<=> (= (Exact-Range ?Relation) ?Range-Class)
(And
(<=> (Holds ?Range-Class ?Range-Instance)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Last ?Tuple) ?Range-Instance))))
(Class ?Range-Class) (Relation ?Relation)))
(=> (= (Exact-Range ?Relation) ?Range-Class)
(Relation ?Relation))
(=> (= (Exact-Range ?Relation) ?Range-Class)
(Class ?Range-Class))
(=> (= (Exact-Range ?Relation) ?Range-Class)
(<=> (Holds ?Range-Class ?Range-Instance)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Last ?Tuple) ?Range-Instance)))))
(Nth-Argument-Name Exact-Range 1 '?Relation))")
)
(make-instance [Total-On] of Relation
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Total-On ?Relation ?Domain-Relation)
(Subrelation-Of (Exact-Domain ?Relation)
?Domain-Relation))
(=>
(Subrelation-Of (Exact-Domain ?Relation)
?Domain-Relation)
(Total-On ?Relation ?Domain-Relation))
(<= (Total-On ?Relation ?Domain-Relation)
(Subrelation-Of (Exact-Domain ?Relation)
?Domain-Relation))
(<=> (Total-On ?Relation ?Domain-Relation)
(Subrelation-Of (Exact-Domain ?Relation)
?Domain-Relation))
(Nth-Argument-Name Total-On 2 '?Domain-Relation)
(Nth-Argument-Name Total-On 1 '?Relation))")
)
(make-instance [Onto] of Relation
(Arity 2)
(Documentation "A relation R is ONTO range class C iff for every element
y in C there
is a tuple in R (x1, x2, ... y).")
(OTHER-AXIOMS "((=> (Onto ?Relation ?Range-Class)
(Subclass-Of (Exact-Range ?Relation) ?Range-Class))
(=> (Subclass-Of (Exact-Range ?Relation) ?Range-Class)
(Onto ?Relation ?Range-Class))
(<= (Onto ?Relation ?Range-Class)
(Subclass-Of (Exact-Range ?Relation) ?Range-Class))
(<=> (Onto ?Relation ?Range-Class)
(Subclass-Of (Exact-Range ?Relation) ?Range-Class))
(Nth-Argument-Name Onto 2 '?Range-Class)
(Nth-Argument-Name Onto 1 '?Relation))")
)
(defclass Unary-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).
A unary relation is a non-empty relation in which all lists have
exactly one item.
<H3>Notes:</H3>
<UL>REDEFINED-IN-FRAME-ONTOLOGY!</UL>
"
(is-a Relation)
(slot OTHER-AXIOMS
(default "((=> (Unary-Relation ?Relation) (= (Arity ?Relation) 1))
(=> (= (Arity ?Relation) 1) (Unary-Relation ?Relation))
(<= (Unary-Relation ?Relation) (= (Arity ?Relation) 1))
(<=> (Unary-Relation ?Relation) (= (Arity ?Relation) 1))
(Nth-Argument-Name Unary-Relation 1 '?Relation)
(=> (Unary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Single ?List)))
(Not (Empty ?R)) (Relation ?R)))
(=>
(And (Forall (?List) (=> (Member ?List ?R) (Single ?List)))
(Not (Empty ?R)) (Relation ?R))
(Unary-Relation ?R))
(<= (Unary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Single ?List)))
(Not (Empty ?R)) (Relation ?R)))
(<=> (Unary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Single ?List)))
(Not (Empty ?R)) (Relation ?R)))
(=> (Unary-Relation ?R)
(Forall (?List) (=> (Member ?List ?R) (Single ?List))))
(=> (Unary-Relation ?R) (Not (Empty ?R)))
(=> (Unary-Relation ?R) (Relation ?R))
(Nth-Argument-Name Unary-Relation 1 '?R))")
(create-accessor read-write))
(single-slot Arity
(create-accessor read-write)
(default (1))
(type Integer))
)
(defclass Binary-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.
A binary relation is a non-empty relation in which all lists have
exactly two items.
<H3>Notes:</H3>
<UL>REDEFINED-IN-FRAME-ONTOLOGY!</UL>
"
(is-a Relation)
(slot OTHER-AXIOMS
(default "((=> (Binary-Relation ?Relation) (= (Arity ?Relation) 2))
(=> (= (Arity ?Relation) 2) (Binary-Relation ?Relation))
(<= (Binary-Relation ?Relation) (= (Arity ?Relation) 2))
(<=> (Binary-Relation ?Relation) (= (Arity ?Relation) 2))
(Nth-Argument-Name Binary-Relation 1 '?Relation)
(=> (Binary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Double ?List)))
(Not (Empty ?R)) (Relation ?R)))
(=>
(And (Forall (?List) (=> (Member ?List ?R) (Double ?List)))
(Not (Empty ?R)) (Relation ?R))
(Binary-Relation ?R))
(<= (Binary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Double ?List)))
(Not (Empty ?R)) (Relation ?R)))
(<=> (Binary-Relation ?R)
(And (Forall (?List) (=> (Member ?List ?R) (Double ?List)))
(Not (Empty ?R)) (Relation ?R)))
(=> (Binary-Relation ?R)
(Forall (?List) (=> (Member ?List ?R) (Double ?List))))
(=> (Binary-Relation ?R) (Not (Empty ?R)))
(=> (Binary-Relation ?R) (Relation ?R))
(Nth-Argument-Name Binary-Relation 1 '?R))")
(create-accessor read-write))
(single-slot Arity
(create-accessor read-write)
(default (2))
(type Integer))
(multislot Composition-Of
(create-accessor read-write)
(type INSTANCE))
(single-slot Inverse
(create-accessor read-write)
(type INSTANCE))
)
(make-instance [Projection] of Function
(Arity 3)
(Function-Arity 2)
(Range Class)
(Documentation "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.")
(OTHER-AXIOMS "((=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(And
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance)))))
(Class ?Projection-Relation) (=< ?Column (Arity
?Relation))
(Positive-Integer ?Column) (Defined (Arity ?Relation))))
(=>
(And
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance)))))
(Class ?Projection-Relation) (=< ?Column (Arity
?Relation))
(Positive-Integer ?Column) (Defined (Arity ?Relation)))
(= (Projection ?Relation ?Column) ?Projection-Relation))
(<= (= (Projection ?Relation ?Column)
?Projection-Relation)
(And
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance)))))
(Class ?Projection-Relation) (=< ?Column (Arity
?Relation))
(Positive-Integer ?Column) (Defined (Arity ?Relation))))
(<=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(And
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance)))))
(Class ?Projection-Relation) (=< ?Column (Arity
?Relation))
(Positive-Integer ?Column) (Defined (Arity ?Relation))))
(=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(Defined (Arity ?Relation)))
(=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(Positive-Integer ?Column))
(=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(=< ?Column (Arity ?Relation)))
(=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(Class ?Projection-Relation))
(=> (= (Projection ?Relation ?Column)
?Projection-Relation)
(Forall (?Projection-Instance)
(<=> (Instance-Of ?Instance ?Projection-Relation)
(Exists (?Tuple)
(And (Member ?Tuple ?Relation)
(= (Nth ?Tuple ?Column) ?Instance))))))
(Nth-Argument-Name Projection 2 '?Column)
(Nth-Argument-Name Projection 1 '?Relation))")
)
(make-instance [Composition-Of] of Relation
(Arity 2)
(Range List)
(Domain Binary-Relation)
(Documentation "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))).
<H3>Notes:</H3>
<UL><B>Example: </B>(=> (composition-of r (listof a b c d)) (= r
(composition d (composition c (composition b a)))))
<BR></UL>")
(OTHER-AXIOMS "((=> (Composition-Of ?Binary-Relation ?List-Of-Relations)
(And
(Or
(And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition (First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists (?Left-Sub-Relation)
(And
(= ?Binary-Relation
(Composition (Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of ?Left-Sub-Relation
(Butlast ?List-Of-Relations)))))
(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
(Not (Null ?List-Of-Relations)) (List
?List-Of-Relations)
(Binary-Relation ?Binary-Relation)))
(=>
(And
(Or
(And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition (First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists (?Left-Sub-Relation)
(And
(= ?Binary-Relation
(Composition (Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of ?Left-Sub-Relation
(Butlast ?List-Of-Relations)))))
(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
(Not (Null ?List-Of-Relations)) (List
?List-Of-Relations)
(Binary-Relation ?Binary-Relation))
(Composition-Of ?Binary-Relation ?List-Of-Relations))
(<= (Composition-Of ?Binary-Relation ?List-Of-Relations)
(And
(Or
(And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition (First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists (?Left-Sub-Relation)
(And
(= ?Binary-Relation
(Composition (Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of ?Left-Sub-Relation
(Butlast ?List-Of-Relations)))))
(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
(Not (Null ?List-Of-Relations)) (List
?List-Of-Relations)
(Binary-Relation ?Binary-Relation)))
(<=> (Composition-Of ?Binary-Relation ?List-Of-Relations)
(And
(Or
(And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition (First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists (?Left-Sub-Relation)
(And
(= ?Binary-Relation
(Composition (Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of ?Left-Sub-Relation
(Butlast ?List-Of-Relations)))))
(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
(Not (Null ?List-Of-Relations)) (List
?List-Of-Relations)
(Binary-Relation ?Binary-Relation)))
(=> (Composition-Of ?Binary-Relation ?List-Of-Relations)
(Or
(And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition (First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists (?Left-Sub-Relation)
(And
(= ?Binary-Relation
(Composition (Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of ?Left-Sub-Relation
(Butlast ?List-Of-Relations))))))
(=> (Item ?R ?List-Of-Relations) (Binary-Relation ?R))
(Not (Null ?List-Of-Relations)) (List ?List-Of-Relations)
(Binary-Relation ?Binary-Relation)
(Nth-Argument-Name Composition-Of 2 '?List-Of-Relations)
(Nth-Argument-Name Composition-Of 1 '?Binary-Relation))")
)
(make-instance [Compose] of Function
(Range Binary-Relation)
(Documentation "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))).
<H3>Notes:</H3>
<UL>version 4 : rewrote to use composition-of. Same meaning as
before</UL>")
(OTHER-AXIOMS "((=> (= (Compose @Binary-Relations) ?Composed-Relation)
(And
(Composition-Of ?Composed-Relation
(Listof @Binary-Relations))
(Binary-Relation ?Composed-Relation)
(Forall (?R)
(=> (Item ?R (Listof @Binary-Relations))
(Binary-Relation ?R)))))
(=>
(And
(Composition-Of ?Composed-Relation
(Listof @Binary-Relations))
(Binary-Relation ?Composed-Relation)
(Forall (?R)
(=> (Item ?R (Listof @Binary-Relations))
(Binary-Relation ?R))))
(= (Compose @Binary-Relations) ?Composed-Relation))
(<= (= (Compose @Binary-Relations) ?Composed-Relation)
(And
(Composition-Of ?Composed-Relation
(Listof @Binary-Relations))
(Binary-Relation ?Composed-Relation)
(Forall (?R)
(=> (Item ?R (Listof @Binary-Relations))
(Binary-Relation ?R)))))
(<=> (= (Compose @Binary-Relations) ?Composed-Relation)
(And
(Composition-Of ?Composed-Relation
(Listof @Binary-Relations))
(Binary-Relation ?Composed-Relation)
(Forall (?R)
(=> (Item ?R (Listof @Binary-Relations))
(Binary-Relation ?R)))))
(=> (= (Compose @Binary-Relations) ?Composed-Relation)
(Forall (?R)
(=> (Item ?R (Listof @Binary-Relations))
(Binary-Relation ?R))))
(=> (= (Compose @Binary-Relations) ?Composed-Relation)
(Binary-Relation ?Composed-Relation))
(=> (= (Compose @Binary-Relations) ?Composed-Relation)
(Composition-Of ?Composed-Relation
(Listof @Binary-Relations)))
(Undefined (Arity Compose))
(Undefined (Function-Arity Compose)))")
)
(make-instance [Alias] of Relation
(Arity 2)
(Range Relation)
(Domain Relation)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Alias ?Relation-1 ?Relation-2)
(And (= ?Relation-1 ?Relation-2) (Relation ?Relation-2)
(Relation ?Relation-1)))
(=>
(And (= ?Relation-1 ?Relation-2) (Relation ?Relation-2)
(Relation ?Relation-1))
(Alias ?Relation-1 ?Relation-2))
(<= (Alias ?Relation-1 ?Relation-2)
(And (= ?Relation-1 ?Relation-2) (Relation ?Relation-2)
(Relation ?Relation-1)))
(<=> (Alias ?Relation-1 ?Relation-2)
(And (= ?Relation-1 ?Relation-2) (Relation ?Relation-2)
(Relation ?Relation-1)))
(=> (Alias ?Relation-1 ?Relation-2)
(= ?Relation-1 ?Relation-2))
(Relation ?Relation-2) (Relation ?Relation-1)
(Nth-Argument-Name Alias 2 '?Relation-2)
(Nth-Argument-Name Alias 1 '?Relation-1))")
)
(make-instance [Domain-Of] of Relation
(Arity 2)
(Documentation "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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>In Cyc, domain-of is called canHaveSlots.
<BR></UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Domain-Of 2 '?Binary-Relation)
(Nth-Argument-Name Domain-Of 1 '?Domain-Class))")
)
(make-instance [Range-Of] of Relation
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((Nth-Argument-Name Range-Of 2 '?Relation)
(Nth-Argument-Name Range-Of 1 '?Type))")
)
(make-instance [Nth-Domain] of Relation
(Arity 3)
(Documentation "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.
<H3>Notes:</H3>
<UL>What about nth-range?
<BR>A range restriction of a function is the same thing as
an nth-domain restriction on the last element of each
tuple, i.e., the values of the function. Therefore
there is no nth-range relation.
<BR></UL>")
(OTHER-AXIOMS "((=> (Nth-Domain ?Relation ?N ?Type)
(And
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type)))
(Class ?Type) (Positive-Integer ?N) (Relation
?Relation)))
(=>
(And
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type)))
(Class ?Type) (Positive-Integer ?N) (Relation
?Relation))
(Nth-Domain ?Relation ?N ?Type))
(<= (Nth-Domain ?Relation ?N ?Type)
(And
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type)))
(Class ?Type) (Positive-Integer ?N) (Relation
?Relation)))
(<=> (Nth-Domain ?Relation ?N ?Type)
(And
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type)))
(Class ?Type) (Positive-Integer ?N) (Relation
?Relation)))
(=> (Nth-Domain ?Relation ?N ?Type)
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Instance-Of (Nth ?Tuple ?N) ?Type))))
(Class ?Type) (Positive-Integer ?N) (Relation ?Relation)
(Nth-Argument-Name Nth-Domain 3 '?Type)
(Nth-Argument-Name Nth-Domain 2 '?N)
(Nth-Argument-Name Nth-Domain 1 '?Relation))")
)
(make-instance [Nth-Argument-Name] of Relation
(Arity 3)
(Documentation "A relation that allows the user to document the
arguments to a relation.
For example, (nth-argument-name child-of 2 '?animal) says that the second
argument to the child-of relation can be spelled ?animal. Note: this is
different from nth-domain; it does not impose a constraint on the
relation,
it merely adds documentation.")
(OTHER-AXIOMS "((Nth-Argument-Name Nth-Argument-Name 3 '?Variable)
(Nth-Argument-Name Nth-Argument-Name 2 '?N)
(Nth-Argument-Name Nth-Argument-Name 1 '?Relation))")
)
(make-instance [Domain-Name] of Function
(Range Variable)
(Domain Slot)
(Arity 2)
(Function-Arity 1)
(Documentation "A relation that allows the user to document the domain
argument of a slot.
For example, (domain-name all-instances '?class) says that the domain
of the slot all-instances can be spelled ?class. Note: this is
different from domain; it does not impose a constraint on the relation,
it merely adds documentation.")
(OTHER-AXIOMS "((=> (= (Domain-Name ?Slot) ?Variable)
(Nth-Argument-Name ?Slot 0 ?Variable))
(Nth-Argument-Name Domain-Name 1 '?Slot))")
)
(make-instance [Range-Name] of Function
(Range Variable)
(Domain Relation)
(Arity 2)
(Function-Arity 1)
(Documentation "A function that allows the user to document the range
variable of a relation.
For example, (range-name child-of '?animal) says that the range of the
child-of relation can be spelled ?animal. Note: this is
different from range; it does not impose a constraint on the relation,
it merely adds documentation. See also nth-argument-name.")
(OTHER-AXIOMS "((Nth-Argument-Name Range-Name 1 '?Relation))")
)
(make-instance [Nth-Domain-Subclass-Of] of Relation
(Arity 3)
(Documentation "A type of domain restrictions generalized to n-ary
relations.
The sentence (nth-domain-subclass-of rel 3 type-class) says that
the 3rd element of each tuple in the relation REL is
a subclass of type-class.")
(OTHER-AXIOMS "((=> (Nth-Domain-Subclass-Of ?Relation ?N ?Type)
(=> (Member ?Tuple ?Relation)
(And (>= (Length ?Tuple) ?N)
(Subclass-Of (Nth ?Tuple ?N) ?Type))))
(Nth-Argument-Name Nth-Domain-Subclass-Of 3 '?Type)
(Nth-Argument-Name Nth-Domain-Subclass-Of 2 '?N)
(Nth-Argument-Name Nth-Domain-Subclass-Of 1 '?Relation))")
)
(make-instance [Range-Subclass-Of] of Relation
(Range Class)
(Domain Relation)
(Arity 2)
(Documentation "(range-subclass-of function class) means that the value
returned by
function is a subclass-of class.")
(OTHER-AXIOMS "((=> (Range-Subclass-Of ?Relation ?Type)
(=> (Member ?Tuple ?Relation)
(And (= (Length ?Tuple) ?N)
(Subclass-Of (Nth ?Tuple ?N) ?Type))))
(Nth-Argument-Name Range-Subclass-Of 2 '?Type)
(Nth-Argument-Name Range-Subclass-Of 1 '?Relation))")
)
(make-instance [Relation-Universe] of Function
(Arity 2)
(Function-Arity 1)
(Range Class)
(Domain Relation)
(Documentation "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.")
(OTHER-AXIOMS "((=> (= (Relation-Universe ?Relation) ?Type-Class)
(And
(<=>
(Exists (?Tuple)
(And (Member ?Tuple ?Relation) (Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class))
(Class ?Type-Class) (Relation ?Relation)))
(=>
(And
(<=>
(Exists (?Tuple)
(And (Member ?Tuple ?Relation) (Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class))
(Class ?Type-Class) (Relation ?Relation))
(= (Relation-Universe ?Relation) ?Type-Class))
(<= (= (Relation-Universe ?Relation) ?Type-Class)
(And
(<=>
(Exists (?Tuple)
(And (Member ?Tuple ?Relation) (Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class))
(Class ?Type-Class) (Relation ?Relation)))
(<=> (= (Relation-Universe ?Relation) ?Type-Class)
(And
(<=>
(Exists (?Tuple)
(And (Member ?Tuple ?Relation) (Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class))
(Class ?Type-Class) (Relation ?Relation)))
(=> (= (Relation-Universe ?Relation) ?Type-Class)
(Relation ?Relation))
(=> (= (Relation-Universe ?Relation) ?Type-Class)
(Class ?Type-Class))
(=> (= (Relation-Universe ?Relation) ?Type-Class)
(<=>
(Exists (?Tuple)
(And (Member ?Tuple ?Relation) (Item ?X ?Tuple)))
(Instance-Of ?X ?Type-Class)))
(Nth-Argument-Name Relation-Universe 1 '?Relation))")
)
(make-instance [All-Values] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "ALL-VALUES is a way to state all of 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.
<H3>Notes:</H3>
<UL><B>Version-4: </B>In version 3, this was incorrectly defined as a
relation.
It should have been a function all along. The definition
remains the same.
<BR></UL>")
(OTHER-AXIOMS "((=>
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values)
(And
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value))
(Binary-Relation ?Binary-Relation)))
(=>
(And
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value))
(Binary-Relation ?Binary-Relation))
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values))
(<=
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values)
(And
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value))
(Binary-Relation ?Binary-Relation)))
(<=>
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values)
(And
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value))
(Binary-Relation ?Binary-Relation)))
(=>
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values)
(Binary-Relation ?Binary-Relation))
(=>
(= (All-Values ?Instance ?Binary-Relation)
?Set-Of-Values)
(<=> (Member ?Value ?Set-Of-Values)
(Holds ?Binary-Relation ?Instance ?Value)))
(Nth-Argument-Name All-Values 2 '?Binary-Relation)
(Nth-Argument-Name All-Values 1 '?Instance))")
)
(make-instance [Obsolete-Value-Type] of Relation
(Arity 3)
(Documentation "The OBSOLETE-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.
<H3>Notes:</H3>
<UL>OBSOLETE-VALUE-TYPE is convenient for specifying type restrictions
on slots relative to a class by using the class's instance
variable.</UL>")
(OTHER-AXIOMS "((=> (Obsolete-Value-Type ?Instance ?Binary-Relation ?Type)
(And
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))
(Class ?Type) (Binary-Relation ?Binary-Relation)))
(=>
(And
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))
(Class ?Type) (Binary-Relation ?Binary-Relation))
(Obsolete-Value-Type ?Instance ?Binary-Relation ?Type))
(<= (Obsolete-Value-Type ?Instance ?Binary-Relation ?Type)
(And
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))
(Class ?Type) (Binary-Relation ?Binary-Relation)))
(<=> (Obsolete-Value-Type ?Instance ?Binary-Relation
?Type)
(And
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type)))
(Class ?Type) (Binary-Relation ?Binary-Relation)))
(=> (Obsolete-Value-Type ?Instance ?Binary-Relation ?Type)
(Forall (?Value)
(=> (Holds ?Binary-Relation ?Instance ?Value)
(Instance-Of ?Value ?Type))))
(Class ?Type) (Binary-Relation ?Binary-Relation)
(Nth-Argument-Name Obsolete-Value-Type 3 '?Type)
(Nth-Argument-Name Obsolete-Value-Type 2
'?Binary-Relation)
(Nth-Argument-Name Obsolete-Value-Type 1 '?Instance))")
)
(make-instance [Obsolete-Same-Values] of Relation
(Arity 3)
(Documentation "Two binary relations R1 and R2 have the
OBSOLETE-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.")
(OTHER-AXIOMS "((=> (Obsolete-Same-Values ?Instance ?Slot1 ?Slot2)
(And
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value))
(Binary-Relation ?Slot2) (Binary-Relation ?Slot1)))
(=>
(And
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value))
(Binary-Relation ?Slot2) (Binary-Relation ?Slot1))
(Obsolete-Same-Values ?Instance ?Slot1 ?Slot2))
(<= (Obsolete-Same-Values ?Instance ?Slot1 ?Slot2)
(And
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value))
(Binary-Relation ?Slot2) (Binary-Relation ?Slot1)))
(<=> (Obsolete-Same-Values ?Instance ?Slot1 ?Slot2)
(And
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value))
(Binary-Relation ?Slot2) (Binary-Relation ?Slot1)))
(=> (Obsolete-Same-Values ?Instance ?Slot1 ?Slot2)
(<=> (Holds ?Slot1 ?Instance ?Value)
(Holds ?Slot2 ?Instance ?Value)))
(Binary-Relation ?Slot2) (Binary-Relation ?Slot1)
(Nth-Argument-Name Obsolete-Same-Values 3 '?Slot2)
(Nth-Argument-Name Obsolete-Same-Values 2 '?Slot1)
(Nth-Argument-Name Obsolete-Same-Values 1 '?Instance))")
)
(make-instance [Obsolete-Slot-Cardinality] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "If a OBSOLETE-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 cardinality for R on all instances of C.
<H3>Notes:</H3>
<UL><B>See-Also: </B>Specifying that the slot cardinality is = to some
integer
is equivalent to using the Loom and CLASSIC `EXACTLY'
operator.
<BR>Note that obsolete-slot-cardinality is a function. That means
that for any domain and relation, there is at most one
integer N that can be the obsolete-slot-cardinality. If there
is
no such fixed number, then the value of the function is
undefined for the given domain and relation.
<BR></UL>")
(OTHER-AXIOMS "((=>
(=> (Instance-Of ?Instance ?Domain-Class)
(Cardinality ?Binary-Relation ?Instance ?N))
(=
(Obsolete-Slot-Cardinality ?Domain-Class
?Binary-Relation)
?N))
(<=
(=
(Obsolete-Slot-Cardinality ?Domain-Class
?Binary-Relation)
?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(Cardinality ?Binary-Relation ?Instance ?N)))
(<=>
(=
(Obsolete-Slot-Cardinality ?Domain-Class
?Binary-Relation)
?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(Cardinality ?Binary-Relation ?Instance ?N)))
(=>
(=
(Obsolete-Slot-Cardinality ?Domain-Class
?Binary-Relation)
?N)
(=> (Instance-Of ?Instance ?Domain-Class)
(Cardinality ?Binary-Relation ?Instance ?N)))
(<=> (= (Obsolete-Slot-Cardinality ?C ?S) ?N)
(Template-Slot-Value Slot-Cardinality ?S ?C ?N))
(Nth-Argument-Name Obsolete-Slot-Cardinality 2
'?Binary-Relation)
(Nth-Argument-Name Obsolete-Slot-Cardinality 1
'?Domain-Class))")
)
(make-instance [Single-Valued-Slot] of Relation
(Arity 2)
(Documentation "The cardinality of the binary relation when applied to
the frame is 1.")
(OTHER-AXIOMS "((=> (Single-Valued-Slot ?Frame ?Binary-Relation)
(Cardinality ?Binary-Relation ?Frame 1))
(=> (Cardinality ?Binary-Relation ?Frame 1)
(Single-Valued-Slot ?Frame ?Binary-Relation))
(<= (Single-Valued-Slot ?Frame ?Binary-Relation)
(Cardinality ?Binary-Relation ?Frame 1))
(<=> (Single-Valued-Slot ?Frame ?Binary-Relation)
(Cardinality ?Binary-Relation ?Frame 1))
(Nth-Argument-Name Single-Valued-Slot 2 '?Binary-Relation)
(Nth-Argument-Name Single-Valued-Slot 1 '?Frame))")
)
(make-instance [Default-Slot-Value] of Relation
(Arity 3)
(OTHER-AXIOMS "((Slot-Of ?Slot ?Frame)
(Nth-Argument-Name Default-Slot-Value 3 '?Value)
(Nth-Argument-Name Default-Slot-Value 2 '?Frame)
(Nth-Argument-Name Default-Slot-Value 1 '?Slot))")
)
(make-instance [Default-Template-Slot-Value] of Relation
(Arity 3)
(OTHER-AXIOMS "((Template-Slot-Of ?Slot ?Class)
(Nth-Argument-Name Default-Template-Slot-Value 3 '?Value)
(Nth-Argument-Name Default-Template-Slot-Value 2 '?Class)
(Nth-Argument-Name Default-Template-Slot-Value 1
'?Slot))")
)
(make-instance [Inherited-Slot-Value] of Relation
(Arity 3)
(Documentation "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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>all-inherited-slot-valuesversion 4: changed
INHERITED-SLOT-VALUES to a relation,
and renamed it to the singular formObsolete. Use
TEMPLATE-SLOT-VALUE instead.</UL>")
(OTHER-AXIOMS "((=> (Inherited-Slot-Value ?Class ?Binary-Relation ?Value)
(Template-Slot-Value ?Binary-Relation ?Class ?Value))
(=> (Template-Slot-Value ?Binary-Relation ?Class ?Value)
(Inherited-Slot-Value ?Class ?Binary-Relation ?Value))
(<= (Inherited-Slot-Value ?Class ?Binary-Relation ?Value)
(Template-Slot-Value ?Binary-Relation ?Class ?Value))
(<=> (Inherited-Slot-Value ?Class ?Binary-Relation ?Value)
(Template-Slot-Value ?Binary-Relation ?Class ?Value))
(Nth-Argument-Name Inherited-Slot-Value 3 '?Value)
(Nth-Argument-Name Inherited-Slot-Value 2
'?Binary-Relation)
(Nth-Argument-Name Inherited-Slot-Value 1 '?Class))")
)
(make-instance [Default-Facet-Value] of Relation
(Arity 4)
(OTHER-AXIOMS "((Slot-Of ?Slot ?Frame)
(Nth-Argument-Name Default-Facet-Value 4 '?Value)
(Nth-Argument-Name Default-Facet-Value 3 '?Frame)
(Nth-Argument-Name Default-Facet-Value 2 '?Slot)
(Nth-Argument-Name Default-Facet-Value 1 '?Facet))")
)
(make-instance [Default-Template-Facet-Value] of Relation
(Arity 4)
(OTHER-AXIOMS "((Template-Facet-Of ?Slot ?Class)
(Nth-Argument-Name Default-Template-Facet-Value 4 '?Value)
(Nth-Argument-Name Default-Template-Facet-Value 3 '?Class)
(Nth-Argument-Name Default-Template-Facet-Value 2 '?Slot)
(Nth-Argument-Name Default-Template-Facet-Value 1
'?Facet))")
)
(make-instance [Inherited-Facet-Value] of Relation
(Arity 4)
(Documentation "
<H3>Notes:</H3>
<UL>Obsolete. Use TEMPLATE-FACET-VALUE instead.</UL>")
(OTHER-AXIOMS "((=>
(Inherited-Facet-Value ?Facet ?Class ?Binary-Relation
?Value)
(Template-Facet-Value ?Facet ?Binary-Relation ?Class
?Value))
(=>
(Template-Facet-Value ?Facet ?Binary-Relation ?Class
?Value)
(Inherited-Facet-Value ?Facet ?Class ?Binary-Relation
?Value))
(<=
(Inherited-Facet-Value ?Facet ?Class ?Binary-Relation
?Value)
(Template-Facet-Value ?Facet ?Binary-Relation ?Class
?Value))
(<=>
(Inherited-Facet-Value ?Facet ?Class ?Binary-Relation
?Value)
(Template-Facet-Value ?Facet ?Binary-Relation ?Class
?Value))
(Nth-Argument-Name Inherited-Facet-Value 4 '?Value)
(Nth-Argument-Name Inherited-Facet-Value 3
'?Binary-Relation)
(Nth-Argument-Name Inherited-Facet-Value 2 '?Class)
(Nth-Argument-Name Inherited-Facet-Value 1 '?Facet))")
)
(defclass Class-Partition "A set of mutually disjoint classes. Disjointness
of
classes is a special case of disjointness of sets."
(is-a Set)
(slot OTHER-AXIOMS
(default "((=> (Class-Partition ?Set-Of-Classes)
(And
(=>
(And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes) (Not (= ?C1 ?C2)))
(Disjoint ?C1 ?C2))
(=> (Member ?C ?Set-Of-Classes) (Class ?C))
(Set ?Set-Of-Classes)))
(=>
(And
(=>
(And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes) (Not (= ?C1 ?C2)))
(Disjoint ?C1 ?C2))
(=> (Member ?C ?Set-Of-Classes) (Class ?C))
(Set ?Set-Of-Classes))
(Class-Partition ?Set-Of-Classes))
(<= (Class-Partition ?Set-Of-Classes)
(And
(=>
(And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes) (Not (= ?C1 ?C2)))
(Disjoint ?C1 ?C2))
(=> (Member ?C ?Set-Of-Classes) (Class ?C))
(Set ?Set-Of-Classes)))
(<=> (Class-Partition ?Set-Of-Classes)
(And
(=>
(And (Member ?C1 ?Set-Of-Classes)
(Member ?C2 ?Set-Of-Classes) (Not (= ?C1 ?C2)))
(Disjoint ?C1 ?C2))
(=> (Member ?C ?Set-Of-Classes) (Class ?C))
(Set ?Set-Of-Classes)))
(=> (Class-Partition ?Set-Of-Classes)
(=>
(And (Member ?C1 ?Set-Of-Classes) (Member ?C2
?Set-Of-Classes)
(Not (= ?C1 ?C2)))
(Disjoint ?C1 ?C2)))
(=> (Class-Partition ?Set-Of-Classes)
(=> (Member ?C ?Set-Of-Classes) (Class ?C)))
(=> (Class-Partition ?Set-Of-Classes) (Set ?Set-Of-Classes))
(Nth-Argument-Name Class-Partition 1 '?Set-Of-Classes))")
(create-accessor read-write))
)
(make-instance [Exhaustive-Decomposition] of Relation
(Domain Class)
(Arity 2)
(Documentation "An exhaustive decomposition of a class C is a set of
subclasses of C such that there cannot be another subclass of the class
that is not in the set (or is a subclass of a class in the set.
Note: this does not necessarily mean that the elements of the set are
disjoint (see partition - a partition is a disjoint exhaustive
decomposition.")
(OTHER-AXIOMS "((=> (Exhaustive-Decomposition ?C ?Decomposition)
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C)))
(Nth-Argument-Name Exhaustive-Decomposition 2
'?Decomposition)
(Nth-Argument-Name Exhaustive-Decomposition 1 '?C))")
)
(make-instance [Disjoint-Decomposition] of Relation
(Arity 2)
(Range Class-Partition)
(Domain Class)
(Documentation "A disjoint-decomposition of a class C is a set of
subclasses of C that are mutually disjoint.
(Used to be called Subclass-Partition)
<H3>Notes:</H3>
<UL>Why is the second argument a set, rather than a sequence
variable?
<BR>Interesting design choice. The ``notation'' question
here is not new syntax for a language, it's just the
definition of a
particular relation called disjoint-decomposition. In KIF you
can define
relations that take an arbitrary number of arguments, using a
\"sequence variable\" that acts like &rest in Lisp. So I
could have made the disjoint-decomposition relation take a
variable number of arguments. I decided not to use a
sequence variable because that is not a minimal ontological
commitment; it imposes an extra logical constraint for the
sake of syntactic convenience. A sequence (list) imposes an
order. But a class-partition requires no order among the
classes. And I wanted the second argument to
disjoint-decomposition to be a class-partition -- a thing that
is defined independently as a set of classes.
<BR></UL>")
(OTHER-AXIOMS "((=> (Disjoint-Decomposition ?C ?Decomposition)
(And
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C))
(Class-Partition ?Decomposition) (Class ?C)))
(=>
(And
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C))
(Class-Partition ?Decomposition) (Class ?C))
(Disjoint-Decomposition ?C ?Decomposition))
(<= (Disjoint-Decomposition ?C ?Decomposition)
(And
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C))
(Class-Partition ?Decomposition) (Class ?C)))
(<=> (Disjoint-Decomposition ?C ?Decomposition)
(And
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C))
(Class-Partition ?Decomposition) (Class ?C)))
(=> (Disjoint-Decomposition ?C ?Decomposition)
(=> (Member ?Subclass ?Decomposition)
(Subclass-Of ?Subclass ?C)))
(Class-Partition ?Decomposition) (Class ?C)
(Nth-Argument-Name Disjoint-Decomposition 2
'?Decomposition)
(Nth-Argument-Name Disjoint-Decomposition 1 '?C))")
)
(make-instance [Partition] of Relation
(Arity 2)
(Subrelation-Of Exhaustive-Decomposition Disjoint-Decomposition)
(Documentation "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. (Used to be called Exhaustive-Subclass-Partition)")
(OTHER-AXIOMS "((=> (Partition ?C ?Class-Partition)
(And
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass ?Class-Partition)
(Member ?Instance ?Subclass))))
(Disjoint-Decomposition ?C ?Class-Partition)))
(=>
(And
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass ?Class-Partition)
(Member ?Instance ?Subclass))))
(Disjoint-Decomposition ?C ?Class-Partition))
(Partition ?C ?Class-Partition))
(<= (Partition ?C ?Class-Partition)
(And
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass ?Class-Partition)
(Member ?Instance ?Subclass))))
(Disjoint-Decomposition ?C ?Class-Partition)))
(<=> (Partition ?C ?Class-Partition)
(And
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass ?Class-Partition)
(Member ?Instance ?Subclass))))
(Disjoint-Decomposition ?C ?Class-Partition)))
(=> (Partition ?C ?Class-Partition)
(=> (Instance-Of ?Instance ?C)
(Exists (?Subclass)
(And (Member ?Subclass ?Class-Partition)
(Member ?Instance ?Subclass)))))
(=> (Partition ?C ?Class-Partition)
(Disjoint-Decomposition ?C ?Class-Partition))
(Nth-Argument-Name Partition 2 '?Class-Partition)
(Nth-Argument-Name Partition 1 '?C)
(<= (Disjoint-Decomposition @Arg-List) (Partition
@Arg-List))
(<= (Exhaustive-Decomposition @Arg-List)
(Partition @Arg-List)))")
)
(defclass Symmetric-Relation "Relation R is symmetric if R(x,y) implies
R(y,x)."
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Symmetric-Relation ?R)
(And (=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))
(Binary-Relation ?R)))
(=>
(And (=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))
(Binary-Relation ?R))
(Symmetric-Relation ?R))
(<= (Symmetric-Relation ?R)
(And (=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))
(Binary-Relation ?R)))
(<=> (Symmetric-Relation ?R)
(And (=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))
(Binary-Relation ?R)))
(=> (Symmetric-Relation ?R)
(=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(=> (Symmetric-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Symmetric-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass 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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>asymmetric-relation</UL>"
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Antisymmetric-Relation ?R)
(And (=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)) (= ?X ?Y))
(Binary-Relation ?R)))
(=>
(And (=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)) (= ?X ?Y))
(Binary-Relation ?R))
(Antisymmetric-Relation ?R))
(<= (Antisymmetric-Relation ?R)
(And (=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)) (= ?X ?Y))
(Binary-Relation ?R)))
(<=> (Antisymmetric-Relation ?R)
(And (=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)) (= ?X ?Y))
(Binary-Relation ?R)))
(=> (Antisymmetric-Relation ?R)
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)) (= ?X ?Y)))
(=> (Antisymmetric-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Antisymmetric-Relation 1 '?R))")
(create-accessor read-write))
)
;;; Forward declaration for external reference Irreflexive-Relation.
;;; Forward declaration for Irreflexive-Relation.
(loom:defconcept Irreflexive-Relation :only-if-no-preexisting-definition-p
common-lisp:t)
(defclass Asymmetric-Relation "A binary relation is asymmetric if it is
antisymmetric
and irreflexive over its exact-domain."
(is-a Irreflexive-Relation Antisymmetric-Relation)
(slot OTHER-AXIOMS
(default "((=> (Asymmetric-Relation ?R)
(And (Irreflexive-Relation ?R) (Antisymmetric-Relation ?R)))
(=> (And (Irreflexive-Relation ?R) (Antisymmetric-Relation
?R))
(Asymmetric-Relation ?R))
(<= (Asymmetric-Relation ?R)
(And (Irreflexive-Relation ?R) (Antisymmetric-Relation ?R)))
(<=> (Asymmetric-Relation ?R)
(And (Irreflexive-Relation ?R) (Antisymmetric-Relation ?R)))
(=> (Asymmetric-Relation ?R) (Irreflexive-Relation ?R))
(=> (Asymmetric-Relation ?R) (Antisymmetric-Relation ?R))
(Nth-Argument-Name Asymmetric-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Reflexive-Relation "Relation R is reflexive if R(x,x) for all x in
the domain of R."
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Reflexive-Relation ?R)
(And (=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X
?X))
(Binary-Relation ?R)))
(=>
(And (=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X
?X))
(Binary-Relation ?R))
(Reflexive-Relation ?R))
(<= (Reflexive-Relation ?R)
(And (=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X
?X))
(Binary-Relation ?R)))
(<=> (Reflexive-Relation ?R)
(And (=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X
?X))
(Binary-Relation ?R)))
(=> (Reflexive-Relation ?R)
(=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X ?X)))
(=> (Reflexive-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Reflexive-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Irreflexive-Relation "Relation R is irreflexive if if R(a,a) never
holds.
<H3>Notes:</H3>
<UL>This is a change in definition. Used to mean (not
reflexive).<B>Formerly: </B>antireflexive-relation</UL>"
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Irreflexive-Relation ?R)
(And (Forall (?X) (Not (Holds ?R ?X ?X)))
(Binary-Relation ?R)))
(=>
(And (Forall (?X) (Not (Holds ?R ?X ?X))) (Binary-Relation
?R))
(Irreflexive-Relation ?R))
(<= (Irreflexive-Relation ?R)
(And (Forall (?X) (Not (Holds ?R ?X ?X)))
(Binary-Relation ?R)))
(<=> (Irreflexive-Relation ?R)
(And (Forall (?X) (Not (Holds ?R ?X ?X)))
(Binary-Relation ?R)))
(=> (Irreflexive-Relation ?R)
(Forall (?X) (Not (Holds ?R ?X ?X))))
(=> (Irreflexive-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Irreflexive-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Transitive-Relation "Relation R is transitive if R(x,y) and R(y,z)
implies R(x,z)."
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z)) (Holds ?R ?X
?Z))
(Binary-Relation ?R)))
(=>
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z)) (Holds ?R ?X
?Z))
(Binary-Relation ?R))
(Transitive-Relation ?R))
(<= (Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z)) (Holds ?R ?X
?Z))
(Binary-Relation ?R)))
(<=> (Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z)) (Holds ?R ?X
?Z))
(Binary-Relation ?R)))
(=> (Transitive-Relation ?R)
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z)) (Holds ?R ?X
?Z)))
(=> (Transitive-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Transitive-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Weak-Transitive-Relation "Relation R is weak-transitive if R(x,y)
and R(y,z) and x /= z implies
R(x,z)."
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Weak-Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z) (Not (= ?X ?Z)))
(Holds ?R ?X ?Z))
(Binary-Relation ?R)))
(=>
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z) (Not (= ?X ?Z)))
(Holds ?R ?X ?Z))
(Binary-Relation ?R))
(Weak-Transitive-Relation ?R))
(<= (Weak-Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z) (Not (= ?X ?Z)))
(Holds ?R ?X ?Z))
(Binary-Relation ?R)))
(<=> (Weak-Transitive-Relation ?R)
(And
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z) (Not (= ?X ?Z)))
(Holds ?R ?X ?Z))
(Binary-Relation ?R)))
(=> (Weak-Transitive-Relation ?R)
(=> (And (Holds ?R ?X ?Y) (Holds ?R ?Y ?Z) (Not (= ?X ?Z)))
(Holds ?R ?X ?Z)))
(=> (Weak-Transitive-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Weak-Transitive-Relation 1 '?R))")
(create-accessor read-write))
)
;;; Forward declaration for external reference Unary-Function.
;;; Forward declaration for Unary-Function.
(loom:defconcept Unary-Function :only-if-no-preexisting-definition-p
common-lisp:t)
(defclass One-To-One-Relation
(is-a Unary-Function)
(slot OTHER-AXIOMS
(default "((=> (One-To-One-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Unary-Function ?R)))
(=>
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Unary-Function ?R))
(One-To-One-Relation ?R))
(<= (One-To-One-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Unary-Function ?R)))
(<=> (One-To-One-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Unary-Function ?R)))
(=> (One-To-One-Relation ?R) (Value-Type Inverse ?R
Function))
(=> (One-To-One-Relation ?R) (Cardinality Inverse ?R 1))
(=> (One-To-One-Relation ?R) (Unary-Function ?R))
(Nth-Argument-Name One-To-One-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Many-To-One-Relation
(is-a Function Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Many-To-One-Relation ?R)
(And (Function ?R) (Binary-Relation ?R)))
(=> (And (Function ?R) (Binary-Relation ?R))
(Many-To-One-Relation ?R))
(<= (Many-To-One-Relation ?R)
(And (Function ?R) (Binary-Relation ?R)))
(<=> (Many-To-One-Relation ?R)
(And (Function ?R) (Binary-Relation ?R)))
(=> (Many-To-One-Relation ?R) (Function ?R))
(=> (Many-To-One-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Many-To-One-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass One-To-Many-Relation
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (One-To-Many-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(=>
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R))
(One-To-Many-Relation ?R))
(<= (One-To-Many-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(<=> (One-To-Many-Relation ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(=> (One-To-Many-Relation ?R) (Value-Type Inverse ?R
Function))
(=> (One-To-Many-Relation ?R) (Cardinality Inverse ?R 1))
(=> (One-To-Many-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name One-To-Many-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Many-To-Many-Relation
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Many-To-Many-Relation ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(=>
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R))
(Many-To-Many-Relation ?R))
(<= (Many-To-Many-Relation ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(<=> (Many-To-Many-Relation ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(=> (Many-To-Many-Relation ?R) (Not (Function (Inverse ?R))))
(=> (Many-To-Many-Relation ?R) (Not (Function ?R)))
(=> (Many-To-Many-Relation ?R) (Binary-Relation ?R))
(Nth-Argument-Name Many-To-Many-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Equivalence-Relation "A relation is an equivalence relation if it
is reflexive,
symmetric, and transitive."
(is-a Transitive-Relation Symmetric-Relation Reflexive-Relation)
(slot OTHER-AXIOMS
(default "((=> (Equivalence-Relation ?R)
(And (Transitive-Relation ?R) (Symmetric-Relation ?R)
(Reflexive-Relation ?R)))
(=>
(And (Transitive-Relation ?R) (Symmetric-Relation ?R)
(Reflexive-Relation ?R))
(Equivalence-Relation ?R))
(<= (Equivalence-Relation ?R)
(And (Transitive-Relation ?R) (Symmetric-Relation ?R)
(Reflexive-Relation ?R)))
(<=> (Equivalence-Relation ?R)
(And (Transitive-Relation ?R) (Symmetric-Relation ?R)
(Reflexive-Relation ?R)))
(=> (Equivalence-Relation ?R) (Transitive-Relation ?R))
(=> (Equivalence-Relation ?R) (Symmetric-Relation ?R))
(=> (Equivalence-Relation ?R) (Reflexive-Relation ?R))
(Nth-Argument-Name Equivalence-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass Partial-Order-Relation "A relation is an partial-order if it is
reflexive,
asymmetric, and transitive."
(is-a Transitive-Relation Antisymmetric-Relation Reflexive-Relation)
(slot OTHER-AXIOMS
(default "((=> (Partial-Order-Relation ?R)
(And (Transitive-Relation ?R) (Antisymmetric-Relation ?R)
(Reflexive-Relation ?R)))
(=>
(And (Transitive-Relation ?R) (Antisymmetric-Relation ?R)
(Reflexive-Relation ?R))
(Partial-Order-Relation ?R))
(<= (Partial-Order-Relation ?R)
(And (Transitive-Relation ?R) (Antisymmetric-Relation ?R)
(Reflexive-Relation ?R)))
(<=> (Partial-Order-Relation ?R)
(And (Transitive-Relation ?R) (Antisymmetric-Relation ?R)
(Reflexive-Relation ?R)))
(=> (Partial-Order-Relation ?R) (Transitive-Relation ?R))
(=> (Partial-Order-Relation ?R) (Antisymmetric-Relation ?R))
(=> (Partial-Order-Relation ?R) (Reflexive-Relation ?R))
(Nth-Argument-Name Partial-Order-Relation 1 '?R))")
(create-accessor read-write))
)
(defclass 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."
(is-a Partial-Order-Relation)
(slot OTHER-AXIOMS
(default "((=> (Total-Order-Relation ?R)
(And
(=>
(And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(Partial-Order-Relation ?R)))
(=>
(And
(=>
(And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(Partial-Order-Relation ?R))
(Total-Order-Relation ?R))
(<= (Total-Order-Relation ?R)
(And
(=>
(And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(Partial-Order-Relation ?R)))
(<=> (Total-Order-Relation ?R)
(And
(=>
(And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))
(Partial-Order-Relation ?R)))
(=> (Total-Order-Relation ?R)
(=>
(And (Instance-Of ?X (Exact-Domain ?R))
(Instance-Of ?Y (Exact-Domain ?R)))
(Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))))
(=> (Total-Order-Relation ?R) (Partial-Order-Relation ?R))
(Nth-Argument-Name Total-Order-Relation 1 '?R))")
(create-accessor read-write))
)
(make-instance [Documentation] of Relation
(Range String)
(Arity 2)
(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.")
(OTHER-AXIOMS "((Nth-Argument-Name Documentation 2 '?String)
(Nth-Argument-Name Documentation 1 '?Object))")
)
(make-instance [Related-Axioms] of Relation
(Range Sentence)
(Arity 2)
(Documentation "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.
<H3>Notes:</H3>
<UL>Related-Axioms is used by Ontolingua translators to
denote axioms related to a class, relation or instance
that cannot be formulated using the frame ontology.Related-axioms is
multivalued relation (as opposed to
a function). When viewed as a slot, each slot value
is a single axioms (typically specified as quoted
list).Related-axioms is not the same as defining-axiom.
Defining-axiom maps a _constant_ (e.g., a symbol)
to an axiom.<B>See-Also: </B>sentencedefining-axiom</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Related-Axioms 2 '?Sentence)
(Nth-Argument-Name Related-Axioms 1 '?Object))")
)
(make-instance [Slot-Documentation] of Relation
(Alias Documentation-In-Frame)
(Arity 3)
(Documentation "The SLOT-DOCUMENTATION facet associates a documentation
string with a slot on an instance. It allows
you to provide documentation for polymorphic
definitions. Obsolete. Use DOCUMENTATION-IN-FRAME instead.")
(OTHER-AXIOMS "((Nth-Argument-Name Slot-Documentation 3 '?Value)
(Nth-Argument-Name Slot-Documentation 2 '?Frame)
(Nth-Argument-Name Slot-Documentation 1 '?Slot))")
)
(make-instance [Has-Instance] of Relation
(Alias Type-Of)
(Arity 2)
(Documentation "The inverse relation for INSTANCE-OF. (Obsolete, use
Type-of instead).")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Instance 2 '?Individual)
(Nth-Argument-Name Has-Instance 1 '?Class))")
)
(make-instance [Has-Author] of Relation
(Arity 2)
(Documentation "The creator(s) of a creative work.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Author 2 '?Author)
(Nth-Argument-Name Has-Author 1 '?Doc))")
)
(make-instance [Has-Source] of Relation
(Arity 2)
(Documentation "The source from which the snippet of knowledge ?thing
was derived.
For example one might say
(has-source '<<some interesting sentence>> \"Encycloaedia
Britannica.\").")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Source 2 '?Source)
(Nth-Argument-Name Has-Source 1 '?Thing))")
)
;;; Translation of definitions in included ontology Kif-Numbers
;;; into target language Clips
(defclass Number "Number"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Number 1 '?X))")
(create-accessor read-write))
(single-slot Cis
(create-accessor read-write)
(type INSTANCE))
)
(defclass Real-Number "Real number"
(is-a NUMBER)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Real-Number 1 '?X))")
(create-accessor read-write))
)
(defclass Rational-Number "Rational number"
(is-a FLOAT)
(slot OTHER-AXIOMS
(default "((=> (Rational-Number ?X)
(And (Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y))))
(Real-Number ?X)))
(=>
(And (Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y))))
(Real-Number ?X))
(Rational-Number ?X))
(<= (Rational-Number ?X)
(And (Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y))))
(Real-Number ?X)))
(<=> (Rational-Number ?X)
(And (Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y))))
(Real-Number ?X)))
(=> (Rational-Number ?X)
(Exists (?Y) (And (Integer ?Y) (Integer (* ?X ?Y)))))
(=> (Rational-Number ?X) (Real-Number ?X))
(Nth-Argument-Name Rational-Number 1 '?X))")
(create-accessor read-write))
)
(defclass Integer "Integer"
(is-a Rational-Number)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Integer 1 '?X))")
(create-accessor read-write))
)
(defclass Even-Integer "Even integer"
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Even-Integer 1 '?X))")
(create-accessor read-write))
)
(defclass Odd-Integer "Odd integer"
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Odd-Integer 1 '?X))")
(create-accessor read-write))
)
(defclass Natural "Natural number"
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((=> (Natural ?X) (And (> ?X 0) (Integer ?X)))
(=> (And (> ?X 0) (Integer ?X)) (Natural ?X))
(<= (Natural ?X) (And (> ?X 0) (Integer ?X)))
(<=> (Natural ?X) (And (> ?X 0) (Integer ?X)))
(=> (Natural ?X) (> ?X 0)) (=> (Natural ?X) (Integer ?X))
(Nth-Argument-Name Natural 1 '?X))")
(create-accessor read-write))
)
(defclass Nonnegative-Integer "Nonnegative integer"
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((=> (Nonnegative-Integer ?X) (>= ?X 0))
(Nth-Argument-Name Nonnegative-Integer 1 '?X))")
(create-accessor read-write))
)
(defclass Positive "Positive number"
(is-a NUMBER)
(slot OTHER-AXIOMS
(default "((=> (Positive ?X) (> ?X 0)) (Nth-Argument-Name Positive 1
'?X))")
(create-accessor read-write))
)
(defclass Negative "Negative number"
(is-a NUMBER)
(slot OTHER-AXIOMS
(default "((=> (Negative ?X) (< ?X 0)) (Nth-Argument-Name Negative 1
'?X))")
(create-accessor read-write))
)
(defclass Complex-Number "Complex number"
(is-a NUMBER)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Complex-Number 1 '?X))")
(create-accessor read-write))
)
(defclass Zero "The class containing 0. May be used as a predicate."
(is-a INTEGER)
(slot OTHER-AXIOMS
(default "((=> (Zero ?X) (And (= ?X 0) (Integer ?X)))
(=> (And (= ?X 0) (Integer ?X)) (Zero ?X))
(<= (Zero ?X) (And (= ?X 0) (Integer ?X)))
(Template-Slot-Value = Zero 0)
(<=> (Zero ?X) (And (= ?X 0) (Integer ?X)))
(=> (Zero ?X) (Integer ?X)) (Nth-Argument-Name Zero 1 '?X))")
(create-accessor read-write))
)
(make-instance [Logbit] of Relation
(Arity 2)
(Documentation "The sentence {tt (logbit $tau_1$ $tau_2$)} is true if
bit $tau_2$
of $tau_1$ is 1.")
(OTHER-AXIOMS "((Nth-Argument-Name Logbit 2 '?Y)
(Nth-Argument-Name Logbit 1 '?X))")
)
(make-instance [Logtest] of Relation
(Arity 2)
(Documentation "The sentence {tt (logtest $tau_1$ $tau_2$)} is true if
the logical
{it and} of the two's-complement representation of the integers
$tau_1$ and $tau_2$ is not zero.")
(OTHER-AXIOMS "((Nth-Argument-Name Logtest 2 '?Y)
(Nth-Argument-Name Logtest 1 '?X))")
)
(make-instance [*] of Function
(Documentation "If $tau_1$, ..., $tau_n$ denote numbers, then the term
{tt (* $tau_1 ldots tau_n$)} denotes the product of those numbers.")
(OTHER-AXIOMS "((Undefined (Arity *)) (Undefined (Function-Arity *)))")
)
(make-instance [+] of Function
(Documentation "If $tau_1$, ..., $tau_n$ are numerical constants, then
the term
{tt (+ $tau_1 ... tau_n$)} denotes the sum $tau$ of the numbers
corresponding to those constants.")
(OTHER-AXIOMS "((Undefined (Arity +)) (Undefined (Function-Arity +)))")
)
(make-instance [-] of Function
(Documentation "If $tau$ and $tau_1$, ..., $tau_n$ denote numbers, then
the term
{tt (- $tau$ $tau_1 ... tau_n$)} denotes the difference between the
number denoted by $tau$ and the numbers denoted by $tau_1$ through
$tau_n$. An exception occurs when $n=0$, in which case the term
denotes the negation of the number denoted by $tau$.")
(OTHER-AXIOMS "((Undefined (Arity -)) (Undefined (Function-Arity -)))")
)
(make-instance [/] of Function
(Documentation "If $tau_1$, ..., $tau_n$ are numbers, then the term
{tt (/ $tau_1 ... tau_n$)} denotes the result $tau$ obtained by
dividing the number denoted by $tau_1$ by the numbers denoted by
$tau_2$ through $tau_n$. An exception occurs when $n=1$, in which
case the term denotes the reciprocal $tau$ of the number denoted by
$tau_1$.")
(OTHER-AXIOMS "((Undefined (Arity /)) (Undefined (Function-Arity /)))")
)
(make-instance [1+] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (1+ $tau$)} denotes the sum of the object
denoted by
$tau$ and 1.")
(OTHER-AXIOMS "((Nth-Argument-Name 1+ 1 '?X))")
)
(make-instance [1-] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (1- $tau$)} denotes the difference of the
object denoted by
$tau$ and 1.")
(OTHER-AXIOMS "((Nth-Argument-Name 1- 1 '?X))")
)
(make-instance [Abs] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (abs $tau$)} denotes the absolute value of
the object
denoted by $tau$. ")
(OTHER-AXIOMS "((Nth-Argument-Name Abs 1 '?X))")
)
(make-instance [Acos] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "If $tau$ denotes a number, then the term {tt (acos
$tau$)} denotes
the arc cosine of that number (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Acos 1 '?X))")
)
(make-instance [Acosh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (acosh $tau$)} denotes the arc cosine of
the
object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Acosh 1 '?X))")
)
(make-instance [Ash] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (ash $tau_1$ $tau_2$)} denotes the result
of
arithmetically shifting the object denoted by $tau_1$ by the number
of bits denoted by $tau_2$ (left or right shifting depending on the
sign of $tau_2$).")
(OTHER-AXIOMS "((Nth-Argument-Name Ash 1 '?X))")
)
(make-instance [Asin] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (asin $tau$)} denotes the arc sine of the
object
denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Asin 1 '?X))")
)
(make-instance [Asinh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (asinh $tau$)} denotes the hyperbolic arc
sine of the
object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Asinh 1 '?X))")
)
(make-instance [Atan] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (atan $tau$)} denotes the arc tangent of
the object
denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Atan 1 '?X))")
)
(make-instance [Atanh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (atanh $tau$)} denotes the hyperbolic arc
tangent
of the object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Atanh 1 '?X))")
)
(make-instance [Boole] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (boole $tau$ $tau_1$ $tau_2$)} denotes the
result of applying the operation denoted by $tau$ to the objects
denoted by $tau_1$ and $tau_2$.")
(OTHER-AXIOMS "((Nth-Argument-Name Boole 1 '?X))")
)
(make-instance [Ceiling] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "If $tau$ denotes a real number, then the term
{tt (ceiling $tau$)} denotes the smallest integer greater than or
equal to the anumber denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Ceiling 1 '?X))")
)
(make-instance [Cis] of Function
(Range Complex-Number)
(Domain Number)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (cis $tau$)} denotes the complex number
denoted by
$cos(tau) + i sin(tau)$. The argument is any non-complex number of
radians.")
(OTHER-AXIOMS "((=> (= (Cis ?Radians) ?Complex)
(Not (Complex-Number ?Radians)))
(Nth-Argument-Name Cis 1 '?Radians))")
)
(make-instance [Conjugate] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "If $tau$ denotes a complex number, then the term {tt
(conjugate
$tau$)} denotes the complex conjugate of the number denoted by
$tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Conjugate 1 '?C))")
)
(make-instance [Cos] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (cos $tau$)} denotes the cosine of the
object
denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Cos 1 '?X))")
)
(make-instance [Cosh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (cosh $tau$)} denotes the hyperbolic cosine
of the
object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Cosh 1 '?X))")
)
(make-instance [Decode-Float] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (decode-float $tau$)} denotes the mantissa
of the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Decode-Float 1 '?X))")
)
(make-instance [Denominator] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (denominator $tau$)} denotes the
denominator of the
canonical reduced form of the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Denominator 1 '?X))")
)
(make-instance [Exp] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (exp $tau$)} denotes $e$ raised to the
power the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Exp 1 '?X))")
)
;;; --- In the definition of Instance THE-EXPONENTIATION-CONSTANT-E
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Expt] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "{The term {tt (expt $tau_1$ $tau_2$)} denotes the object
denoted by
$tau_1$ raised to the power the object denoted by $tau_2$.}")
(OTHER-AXIOMS "((Nth-Argument-Name Expt 2 '?Power)
(Nth-Argument-Name Expt 1 '?X))")
)
(make-instance [Fceiling] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (fceiling $tau$)} denotes the smallest
integer (as
a floating point number) greater than the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Fceiling 1 '?X))")
)
(make-instance [Ffloor] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (ffloor $tau$)} denotes the largest integer
(as a floating point number) less than the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Ffloor 1 '?X))")
)
(make-instance [Float] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (float $tau$)} denotes the floating point
number
equal to the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Float 1 '?X))")
)
(make-instance [Float-Digits] of Function
(Range Nonnegative-Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (float-digits $tau$)} denotes the number of
digits
used in the representation of a floating point number denoted by
$tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Float-Digits 1 '?X))")
)
(make-instance [Float-Precision] of Function
(Range Nonnegative-Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (float-precision $tau$)} denotes the number
of significant digits
in the floating point number denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Float-Precision 1 '?X))")
)
(make-instance [Float-Radix] of Function
(Range Natural)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (float-radix $tau$)} denotes the radix of
the
floating point number denoted by $tau$. The most common values are 2
and 16.")
(OTHER-AXIOMS "((Nth-Argument-Name Float-Radix 1 '?X))")
)
(make-instance [Float-Sign] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (float-sign $tau_1$ $tau_2$)} denotes a
floating-point
number with the same sign as the object denoted by $tau_1$ and
the same absolute value as the object denoted by $tau_2$.")
(OTHER-AXIOMS "((Nth-Argument-Name Float-Sign 1 '?X))")
)
(make-instance [Floor] of Function
(Range Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (floor $tau$)} denotes the largest integer
less
than the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Floor 1 '?X))")
)
(make-instance [Fround] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (fround $tau$)} is equivalent to {tt
(ffloor (+ 0.5 $tau$))}.")
(OTHER-AXIOMS "((Nth-Argument-Name Fround 1 '?X))")
)
(make-instance [Ftruncate] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (ftruncate $tau$)} denotes the largest
integer (as
a floating point number) less than the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Ftruncate 1 '?X))")
)
(make-instance [Gcd] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (gcd $tau_1 ldots tau_n$)} denotes the
greatest
common divisor of the objects denoted by $tau_1$ through $tau_n$.")
(OTHER-AXIOMS "((Nth-Argument-Name Gcd 1 '?X))")
)
(make-instance [Imagpart] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (imagpart $tau$)} denotes the imaginary
part of the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Imagpart 1 '?X))")
)
(make-instance [Integer-Decode-Float] of Function
(Range Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (integer-decode-float $tau$)} denotes the
significand
of the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Integer-Decode-Float 1 '?X))")
)
(make-instance [Integer-Length] of Function
(Range Nonnegative-Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (integer-length $tau$)} denotes the number
of bits
required to store the absolute magnitude of the object denoted by
$tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Integer-Length 1 '?X))")
)
(make-instance [Isqrt] of Function
(Range Nonnegative-Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (isqrt $tau$)} denotes the integer square
root of the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Isqrt 1 '?X))")
)
(make-instance [Lcm] of Function
(Documentation "The term {tt (lcm $tau_1 ldots tau_n$)} denotes the
least common
multiple of the objects denoted by $tau_1,ldots,tau_n$.")
(OTHER-AXIOMS "((Undefined (Arity Lcm)) (Undefined (Function-Arity
Lcm)))")
)
(make-instance [Log] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (log $tau_1$ $tau_2$)} denotes the
logarithm of the
object denoted by $tau_1$ in the base denoted by $tau_2$.")
(OTHER-AXIOMS "((Nth-Argument-Name Log 2 '?Base)
(Nth-Argument-Name Log 1 '?Number))")
)
(make-instance [Logand] of Function
(Documentation "The term {tt (logand $tau_1 ldots tau_n$)} denotes the
bit-wise
logical and of the objects denoted by $tau_1$ through $tau_n$.")
(OTHER-AXIOMS "((Undefined (Arity Logand))
(Undefined (Function-Arity Logand)))")
)
(make-instance [Logandc1] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (logandc1 $tau_1$ $tau_2$)} is equivalent
to
{tt (logand (lognot $tau_1$) $tau_2$)}.")
(OTHER-AXIOMS "((Nth-Argument-Name Logandc1 2 '?Y)
(Nth-Argument-Name Logandc1 1 '?X))")
)
(make-instance [Logandc2] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (logandc2 $tau_1$ $tau_2$)} is equivalent
to
{tt (logand $tau_1$ (lognot $tau_2$))}.")
(OTHER-AXIOMS "((Nth-Argument-Name Logandc2 2 '?Y)
(Nth-Argument-Name Logandc2 1 '?X))")
)
(make-instance [Logcount] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (logcount $tau$)} denotes the number of {it
on}
bits in the object denoted by $tau$. If the denotation of $tau$ is
positive, then the one bits are counted; otherwise, the zero bits in
the twos-complement representation are counted.")
(OTHER-AXIOMS "((Nth-Argument-Name Logcount 1 '?X))")
)
(make-instance [Logeqv] of Function
(Documentation "The term {tt (logeqv $tau_1 ldots tau_n$)} denotes the
logical-exclusive-or of the objects denoted by
$tau_1,ldots,tau_n$.")
(OTHER-AXIOMS "((Undefined (Arity Logeqv))
(Undefined (Function-Arity Logeqv)))")
)
(make-instance [Logior] of Function
(Documentation "The term {tt (logior $tau_1 ldots tau_n$)} denotes the
bit-wise logical inclusive or of the objects denoted by $tau_1$
through $tau_n$. It denotes 0 if there are no arguments.")
(OTHER-AXIOMS "((Undefined (Arity Logior))
(Undefined (Function-Arity Logior)))")
)
(make-instance [Lognand] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (lognand $tau_1$ $tau_2$)} is equivalent to
{tt (lognot (logand $tau_1$ $tau_2$))}.")
(OTHER-AXIOMS "((Nth-Argument-Name Lognand 2 '?Y)
(Nth-Argument-Name Lognand 1 '?X))")
)
(make-instance [Lognor] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (lognor $tau_1$ $tau_2$)} is equivalent to
{tt (lognot (logior $tau_1$ $tau_2$))}.")
(OTHER-AXIOMS "((Nth-Argument-Name Lognor 2 '?Y)
(Nth-Argument-Name Lognor 1 '?X))")
)
(make-instance [Lognot] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (lognot $tau$)} denotes the bit-wise
logical not of
the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Lognot 1 '?X))")
)
(make-instance [Logorc1] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (logorc1 $tau_1$ $tau_2$)} is equivalent to
{tt (logior (lognot $tau_1$) $tau_2$)}.")
(OTHER-AXIOMS "((Nth-Argument-Name Logorc1 2 '?Y)
(Nth-Argument-Name Logorc1 1 '?X))")
)
(make-instance [Logorc2] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (logorc2 $tau_1$ $tau_2$)} is equivalent to
{tt (logior
$tau_1$ (lognot $tau_2$))}.")
(OTHER-AXIOMS "((Nth-Argument-Name Logorc2 2 '?Y)
(Nth-Argument-Name Logorc2 1 '?X))")
)
(make-instance [Logxor] of Function
(Documentation "The term {tt (logxor $tau_1 ldots tau_n$)} denotes the
bit-wise logical exclusive or of the objects denoted by $tau_1$
through $tau_n$. It denotes 0 if there are no arguments.")
(OTHER-AXIOMS "((Undefined (Arity Logxor))
(Undefined (Function-Arity Logxor)))")
)
(make-instance [Max] of Function
(Documentation "The term {tt (max $tau_1 ldots tau_k$)} denotes the
largest object
denoted by $tau_1$ through $tau_n$.")
(OTHER-AXIOMS "((Undefined (Arity Max)) (Undefined (Function-Arity
Max)))")
)
(make-instance [Min] of Function
(Documentation "The term {tt (min $tau_1 ldots tau_k$)} denotes the
smallest
object denoted by $tau_1$ through $tau_n$.")
(OTHER-AXIOMS "((Undefined (Arity Min)) (Undefined (Function-Arity
Min)))")
)
(make-instance [Mod] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (mod $tau_1$ $tau_2$)} denotes the root of
the object
denoted by $tau_1$ modulo the object denoted by $tau_2$.
The result will have the same sign as denoted by $tau_1$.")
(OTHER-AXIOMS "((Nth-Argument-Name Mod 2 '?Y) (Nth-Argument-Name Mod 1
'?X))")
)
(make-instance [Numerator] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (numerator $tau$)} denotes the numerator of
the
canonical reduced form of the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Numerator 1 '?X))")
)
(make-instance [Phase] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (phase $tau$)} denotes the angle part of
the polar
representation of the object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Phase 1 '?X))")
)
(make-instance [Rationalize] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (rationalize $tau$)} denotes the rational
representation of the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Rationalize 1 '?X))")
)
(make-instance [Realpart] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (realpart $tau$)} denotes the real part of
the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Realpart 1 '?X))")
)
(make-instance [Rem] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (rem <number> <divisor>)} denotes the
remainder of
the object denoted by {tt <number>} divided by the object denoted by
{tt <divisor>}. The result has the same sign as the object denoted
by {tt <divisor>}.")
(OTHER-AXIOMS "((Nth-Argument-Name Rem 2 '?Divisor)
(Nth-Argument-Name Rem 1 '?Number))")
)
(make-instance [Round] of Function
(Range Integer)
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (round $tau$)} denotes the integer nearest
to the
object denoted by $tau$. If the object denoted by $tau$ is halfway
between two integers (for example 3.5), it denotes the nearest integer
divisible by 2.")
(OTHER-AXIOMS "((Nth-Argument-Name Round 1 '?X))")
)
(make-instance [Scale-Float] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The term {tt (scale-float $tau_1$ $tau_2$)} denotes a
floating-point
number that is the representational radix of the object denoted by
$tau_1$ raised to the integer denoted by $tau_2$.")
(OTHER-AXIOMS "((Nth-Argument-Name Scale-Float 2 '?Y)
(Nth-Argument-Name Scale-Float 1 '?X))")
)
(make-instance [Signum] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (signum $tau$)} denotes the sign of the
object
denoted by $tau$. This is one of -1, 1, or 0 for rational numbers
and one of -1.0, 1.0, or 0.0 for floating point numbers.")
(OTHER-AXIOMS "((Nth-Argument-Name Signum 1 '?X))")
)
(make-instance [Sin] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (sin $tau$)} denotes the sine of the object
denoted
by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Sin 1 '?X))")
)
(make-instance [Sinh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (sinh $tau$)} denotes the hyperbolic sine
of the object
denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Sinh 1 '?X))")
)
(make-instance [Sqrt] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (sqrt $tau$)} denotes the principal square
root of the
object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Sqrt 1 '?X))")
)
(make-instance [Tan] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (tan $tau$)} denotes the tangent of the
object denoted
by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Tan 1 '?X))")
)
(make-instance [Tanh] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (tanh $tau$)} denotes the hyperbolic
tangent of the
object denoted by $tau$ (in radians).")
(OTHER-AXIOMS "((Nth-Argument-Name Tanh 1 '?X))")
)
(make-instance [Truncate] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (truncate $tau$)} denotes the largest
integer less
than the object denoted by $tau$.")
(OTHER-AXIOMS "((Nth-Argument-Name Truncate 1 '?X))")
)
(make-instance [<] of Relation
(Arity 2)
(Documentation "The sentence {tt (< $tau_1$ $tau_2$)} is true if and
only if
the number denoted by $tau_1$ is less than the number denoted by
$tau_2$.")
(OTHER-AXIOMS "((Nth-Argument-Name < 2 '?Y) (Nth-Argument-Name < 1 '?X))")
)
(make-instance [>] of Relation
(Arity 2)
(OTHER-AXIOMS "((Nth-Argument-Name > 2 '?Y) (Nth-Argument-Name > 1 '?X))")
)
(make-instance [=<] of Relation
(Arity 2)
(OTHER-AXIOMS "((=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))
(=> (Or (= ?X ?Y) (< ?X ?Y)) (=< ?X ?Y))
(<= (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))
(<=> (=< ?X ?Y) (Or (= ?X ?Y) (< ?X ?Y)))
(Nth-Argument-Name =< 2 '?Y) (Nth-Argument-Name =< 1
'?X))")
)
(make-instance [>=] of Relation
(Arity 2)
(OTHER-AXIOMS "((=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))
(=> (Or (> ?X ?Y) (= ?X ?Y)) (>= ?X ?Y))
(<= (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))
(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))
(Nth-Argument-Name >= 2 '?Y) (Nth-Argument-Name >= 1
'?X))")
)
;;; Translation of definitions in included ontology Kif-Relations
;;; into target language Clips
(defclass 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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>In Loom, relations are called relations.
<BR>In CycL, relations are called relationships.
<BR>In KEE, relations are not supported explicitly.
<BR>In Epikit, relations are called relations.
<BR>In Algernon, relations are called slots.
<BR>What about slots?
<BR>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.
<BR>What about variable-arity relations?
<BR>They are allowed, but need to use a sequence variable in the
definition.
<BR>Originally defined in the KIF-RELATIONS ontology</UL>
<H3>Notes:</H3>
<UL>Functions and relations are defined in the frame ontology.
Inserted here for completeness.</UL>
"
(is-a Thing)
(slot Alias
(create-accessor read-write))
(slot Documentation
(create-accessor read-write))
(slot Domain
(create-accessor read-write))
(slot Onto
(create-accessor read-write))
(slot Range
(create-accessor read-write))
(slot Related-Axioms
(create-accessor read-write))
(slot Subrelation-Of
(create-accessor read-write))
(slot Has-Subrelation
(create-accessor read-write))
(slot Total-On
(create-accessor read-write))
(slot Arity
(create-accessor read-write))
(slot Function-Arity
(create-accessor read-write))
(slot Exact-Domain
(create-accessor read-write))
(slot Exact-Range
(create-accessor read-write))
(slot Relation-Universe
(create-accessor read-write))
(slot OTHER-AXIOMS
(default "((=> (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(=>
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation))
(Relation ?Relation))
(<= (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(<=> (Relation ?Relation)
(And (=> (Member ?Tuple ?Relation) (List ?Tuple))
(Set ?Relation)))
(=> (Relation ?Relation)
(=> (Member ?Tuple ?Relation) (List ?Tuple)))
(=> (Relation ?Relation) (Set ?Relation))
(Nth-Argument-Name Relation 1 '?Relation)
(=> (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(=> (And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set
?R))
(Relation ?R))
(<= (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(<=> (Relation ?R)
(And (Forall (?X) (=> (Member ?X ?R) (List ?X))) (Set ?R)))
(=> (Relation ?R) (Forall (?X) (=> (Member ?X ?R) (List
?X))))
(=> (Relation ?R) (Set ?R)) (Nth-Argument-Name Relation 1
'?R))")
(create-accessor read-write))
(multislot Subrelation-Of
(create-accessor read-write)
(type INSTANCE))
(single-slot Arity
(create-accessor read-write)
(type Integer))
(single-slot Exact-Domain
(create-accessor read-write)
(type INSTANCE))
(single-slot Exact-Range
(create-accessor read-write)
(type INSTANCE))
(multislot Alias
(create-accessor read-write)
(type INSTANCE))
(single-slot Range-Name
(create-accessor read-write)
(type INSTANCE))
(multislot Range-Subclass-Of
(create-accessor read-write)
(type INSTANCE))
(single-slot Relation-Universe
(create-accessor read-write)
(type INSTANCE))
)
(defclass Function "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.
<H3>Notes:</H3>
<UL>Originally defined in the KIF-RELATIONS ontology</UL>
<H3>Notes:</H3>
<UL>Functions and relations are defined in the frame ontology.
Inserted here for completeness.</UL>
"
(is-a RELATION)
(slot OTHER-AXIOMS
(default "((=> (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(=>
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation))
(Function ?Relation))
(<= (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(<=> (Function ?Relation)
(And
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2)))
(Relation ?Relation)))
(=> (Function ?Relation)
(=> (Member ?Tuple1 ?Relation) (Member ?Tuple2 ?Relation)
(= (Butlast ?Tuple1) (Butlast ?Tuple2))
(= (Last ?Tuple1) (Last ?Tuple2))))
(=> (Function ?Relation) (Relation ?Relation))
(Nth-Argument-Name Function 1 '?Relation)
(=> (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(=>
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F))
(Function ?F))
(<= (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(<=> (Function ?F)
(And
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M))))
(Relation ?F)))
(=> (Function ?F)
(Forall (?L ?M)
(=> (Member ?L ?F) (Member ?M ?F)
(= (Butlast ?L) (Butlast ?M)) (= (Last ?L) (Last ?M)))))
(=> (Function ?F) (Relation ?F))
(Nth-Argument-Name Function 1 '?F))")
(create-accessor read-write))
(single-slot Function-Arity
(create-accessor read-write)
(type Integer))
)
;;; --- In the definition of Instance BOTTOM
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Holds] of Relation
(Domain Relation)
(Documentation "If $tau$ denotes a relation, then the sentence
{tt (holds $tau$ $tau_1$ ... $tau_k$)} is true if and only if
the list of objects denoted by $tau_1$,...,$tau_k$ is a member of
that relation.")
(OTHER-AXIOMS "((=> (Holds ?R @Args)
(And (Member (Listof @Args) ?R) (Relation ?R)))
(=> (And (Member (Listof @Args) ?R) (Relation ?R))
(Holds ?R @Args))
(<= (Holds ?R @Args)
(And (Member (Listof @Args) ?R) (Relation ?R)))
(<=> (Holds ?R @Args)
(And (Member (Listof @Args) ?R) (Relation ?R)))
(Undefined (Arity Holds))
(=> (Holds ?R @Args) (Member (Listof @Args) ?R))
(Relation ?R) (Nth-Argument-Name Holds 2 '@Args)
(Nth-Argument-Name Holds 1 '?R))")
)
(make-instance [Value] of Function
(Documentation "If $tau$ denotes a function with a value for the objects
denoted by
$tau_1$,..., $tau_k$, then the term {tt (value $tau$ $tau_1$ ...
$tau_k$)} denotes the value of applying that function to the objects
denoted by $tau_1$,...,$tau_k$. Otherwise, the value is undefined.")
(OTHER-AXIOMS "((Undefined (Arity Value)) (Undefined (Function-Arity
Value))
(Nth-Argument-Name Value 1 '?F))")
)
(make-instance [Apply] of Function
(Arity 3)
(Function-Arity 2)
(OTHER-AXIOMS "((Nth-Argument-Name Apply 2 '?List)
(Nth-Argument-Name Apply 1 '?F))")
)
(make-instance [Map] of Function
(Arity 3)
(Function-Arity 2)
(OTHER-AXIOMS "((Nth-Argument-Name Map 2 '?List)
(Nth-Argument-Name Map 1 '?F))")
)
(make-instance [Universe] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The universe of a relation is the set of all objects
occurring in some
list contained in that relation.")
(OTHER-AXIOMS "((Nth-Argument-Name Universe 1 '?R))")
)
(make-instance [Inverse] of Function
(Arity 2)
(Function-Arity 1)
(Range Binary-Relation)
(Domain Binary-Relation)
(Documentation "One binary relation is the inverse of another if they
are
equivalent when their arguments are swapped. This relation is called
SLOT-INVERSE in the OKBC 2.0 spec.
<H3>Notes:</H3>
<UL>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.originally defined in the KIF-RELATIONS
ontology</UL>" "The inverse of a binary relation is a binary relation with
all
tuples reversed.
<H3>Notes:</H3>
<UL>REDEFINED-IN-FRAME-ONTOLOGY!</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Inverse 1 '?R)
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(=>
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation))
(= (Inverse ?Binary-Relation) ?Inverse-Relation))
(<= (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(<=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(Binary-Relation ?Binary-Relation))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(Binary-Relation ?Inverse-Relation))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X)))
(Nth-Argument-Name Inverse 1 '?Binary-Relation))")
)
(make-instance [Composition] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The composition of a binary relation $r_1$ and a binary
relation $r_2$ is a binary relation in which an object $x$ is related to an
object $z$ if and only if there is an object $y$ such that $x$ is related to
$y$ by $r_1$ and $y$ is related to $z$ by $r_2$.
<H3>Notes:</H3>
<UL>REDEFINED-IN-FRAME-ONTOLOGY!</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Composition 2 '?R2)
(Nth-Argument-Name Composition 1 '?R1))")
)
(defclass One-One
(is-a Function Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (One-One ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Function ?R)
(Binary-Relation ?R)))
(=>
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Function ?R) (Binary-Relation
?R))
(One-One ?R))
(<= (One-One ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Function ?R)
(Binary-Relation ?R)))
(<=> (One-One ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Function ?R)
(Binary-Relation ?R)))
(=> (One-One ?R) (Value-Type Inverse ?R Function))
(=> (One-One ?R) (Cardinality Inverse ?R 1))
(=> (One-One ?R) (Function ?R))
(=> (One-One ?R) (Binary-Relation ?R))
(Nth-Argument-Name One-One 1 '?R))")
(create-accessor read-write))
)
(defclass Many-One
(is-a Function Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Many-One ?R) (And (Function ?R) (Binary-Relation ?R)))
(=> (And (Function ?R) (Binary-Relation ?R)) (Many-One ?R))
(<= (Many-One ?R) (And (Function ?R) (Binary-Relation ?R)))
(<=> (Many-One ?R) (And (Function ?R) (Binary-Relation ?R)))
(=> (Many-One ?R) (Function ?R))
(=> (Many-One ?R) (Binary-Relation ?R))
(Nth-Argument-Name Many-One 1 '?R))")
(create-accessor read-write))
)
(defclass One-Many
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (One-Many ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(=>
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R))
(One-Many ?R))
(<= (One-Many ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(<=> (One-Many ?R)
(And (Value-Type Inverse ?R Function)
(Cardinality Inverse ?R 1) (Binary-Relation ?R)))
(=> (One-Many ?R) (Value-Type Inverse ?R Function))
(=> (One-Many ?R) (Cardinality Inverse ?R 1))
(=> (One-Many ?R) (Binary-Relation ?R))
(Nth-Argument-Name One-Many 1 '?R))")
(create-accessor read-write))
)
(defclass Many-Many
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((=> (Many-Many ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(=>
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R))
(Many-Many ?R))
(<= (Many-Many ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(<=> (Many-Many ?R)
(And (Not (Function (Inverse ?R))) (Not (Function ?R))
(Binary-Relation ?R)))
(=> (Many-Many ?R) (Not (Function (Inverse ?R))))
(=> (Many-Many ?R) (Not (Function ?R)))
(=> (Many-Many ?R) (Binary-Relation ?R))
(Nth-Argument-Name Many-Many 1 '?R))")
(create-accessor read-write))
)
(defclass Unary-Function "A unary function is a function with a single
argument and a single
value. Hence, it is also a binary relation."
(is-a Binary-Relation Function)
(slot OTHER-AXIOMS
(default "((=> (Unary-Function ?F)
(And (Binary-Relation ?F) (Function ?F)))
(=> (And (Binary-Relation ?F) (Function ?F))
(Unary-Function ?F))
(<= (Unary-Function ?F)
(And (Binary-Relation ?F) (Function ?F)))
(<=> (Unary-Function ?F)
(And (Binary-Relation ?F) (Function ?F)))
(=> (Unary-Function ?F) (Binary-Relation ?F))
(=> (Unary-Function ?F) (Function ?F))
(Nth-Argument-Name Unary-Function 1 '?F))")
(create-accessor read-write))
)
(defclass Binary-Function "A binary function is a function with two
arguments and one value. Hence, it
is a relation with three arguments."
(is-a Function)
(slot OTHER-AXIOMS
(default "((=> (Binary-Function ?F)
(And (Forall (?List) (=> (Member ?List ?F) (Triple ?List)))
(Not (Empty ?F)) (Function ?F)))
(=>
(And (Forall (?List) (=> (Member ?List ?F) (Triple ?List)))
(Not (Empty ?F)) (Function ?F))
(Binary-Function ?F))
(<= (Binary-Function ?F)
(And (Forall (?List) (=> (Member ?List ?F) (Triple ?List)))
(Not (Empty ?F)) (Function ?F)))
(<=> (Binary-Function ?F)
(And (Forall (?List) (=> (Member ?List ?F) (Triple ?List)))
(Not (Empty ?F)) (Function ?F)))
(=> (Binary-Function ?F)
(Forall (?List) (=> (Member ?List ?F) (Triple ?List))))
(=> (Binary-Function ?F) (Not (Empty ?F)))
(=> (Binary-Function ?F) (Function ?F))
(Nth-Argument-Name Binary-Function 1 '?F))")
(create-accessor read-write))
)
;;; Translation of definitions in included ontology Okbc-Ontology
;;; into target language Clips
;;; --- In the definition of Class PRIMITIVE
;;;
;;; Can't translate second order classes (aka metaclasses) into CLIPS.
;;;
(defclass Slot
(is-a Binary-Relation)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Slot 1 '?Slot))")
(create-accessor read-write))
(multislot Slot-Same-Values
(create-accessor read-write))
(multislot Slot-Minimum-Cardinality
(create-accessor read-write))
(multislot Slot-Maximum-Cardinality
(create-accessor read-write))
(multislot Slot-Cardinality
(create-accessor read-write))
(multislot Slot-Collection-Type
(create-accessor read-write))
(multislot Slot-Some-Values
(create-accessor read-write))
(multislot Slot-Numeric-Maximum
(create-accessor read-write))
(multislot Slot-Numeric-Minimum
(create-accessor read-write))
(multislot Slot-Subset-Of-Values
(create-accessor read-write))
(multislot Slot-Not-Same-Values
(create-accessor read-write))
(multislot Range
(create-accessor read-write))
(multislot Domain
(create-accessor read-write)
(type INSTANCE))
(single-slot Domain-Name
(create-accessor read-write)
(type INSTANCE))
)
(defclass 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.
<H3>Notes:</H3>
<UL>Version 4: moved THING from the KIF ontology into the frame
ontology.
It isn't defined in the KIF spec, and mainly serves to clarify the
relationship between sets and classes.</UL>"
(is-a INITIAL-OBJECT)
(slot OTHER-AXIOMS
(create-accessor read-write))
(slot DOCUMENTATION
(create-accessor read-write))
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Thing 1 '?X))")
(create-accessor read-write))
)
(defclass Frame "Instances of FRAME are OKBC frames."
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Frame 1 '?X))")
(create-accessor read-write))
)
(defclass Individual "An individual 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. 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).
An individual is something that is not a set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>
"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Individual ?X) (And (Not (Class ?X)) (Thing ?X)))
(=> (And (Not (Class ?X)) (Thing ?X)) (Individual ?X))
(<= (Individual ?X) (And (Not (Class ?X)) (Thing ?X)))
(<=> (Individual ?X) (And (Not (Class ?X)) (Thing ?X)))
(=> (Individual ?X) (Not (Class ?X)))
(=> (Individual ?X) (Thing ?X))
(=> (Individual ?X) (Not (Set ?X)))
(=> (Not (Set ?X)) (Individual ?X))
(<= (Individual ?X) (Not (Set ?X)))
(<=> (Individual ?X) (Not (Set ?X)))
(Nth-Argument-Name Individual 1 '?X))")
(create-accessor read-write))
)
(make-instance [Instance-Of] of Relation
(Arity 2)
(Range Class)
(Documentation "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 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.
<H3>Notes:</H3>
<UL>Why not call instance-of `member-of'?
<BR>Because instance-of is in common usage, and member-of can get
confused
with the set and list operators.
<BR>Why not call instance-of `example-of', or `isa'?
<BR>Because these
words
are used to mean many different things in different contexts.
<BR><B>See-Also: </B>In Cyc, instance-of is called #%allInstanceOf.
<BR>In KEE, instance-of is called member.of.
<BR>In Loom, instance-of is implicit in the syntax (unary predicates).
<BR>In Epikit, there is no notion of instances, although by convention
people use unary relations to denote instance-of relationships.
<BR><B>See-Also: </B>direct-instance-of</UL>")
(OTHER-AXIOMS "((=> (Instance-Of ?Individual ?Class)
(And (Holds ?Class ?Individual) (Class ?Class)))
(=> (And (Holds ?Class ?Individual) (Class ?Class))
(Instance-Of ?Individual ?Class))
(<= (Instance-Of ?Individual ?Class)
(And (Holds ?Class ?Individual) (Class ?Class)))
(<=> (Instance-Of ?Individual ?Class)
(And (Holds ?Class ?Individual) (Class ?Class)))
(=> (Instance-Of ?Individual ?Class)
(Holds ?Class ?Individual))
(Class ?Class) (Nth-Argument-Name Instance-Of 2 '?Class)
(Nth-Argument-Name Instance-Of 1 '?Individual))")
)
(make-instance [Type-Of] of Relation
(Arity 2)
(Documentation "The inverse relation for INSTANCE-OF.
This used to be called HAS-INSTANCE.
<H3>Notes:</H3>
<UL>From OKBC 2.0</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Type-Of 2 '?Individual)
(Nth-Argument-Name Type-Of 1 '?Class))")
)
(make-instance [Subclass-Of] of Relation
(Arity 2)
(Documentation "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.
<H3>Notes:</H3>
<UL><B>See-Also: </B>direct-subclass-of<B>See-Also: </B>In CycL, subclass-of
is called #%allGenls because it is a slot from
a collection to all of its generalizations (superclasses).
<BR>In the KL-ONE literature, subclass relationships are also called
subsumption relationships and ISA is sometimes used for
subclass-of.
<BR>Why is it called Subclass-of instead of subclass or superclass?
<BR>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'.
<BR></UL>")
(OTHER-AXIOMS "((=> (Subclass-Of ?Child-Class ?Parent-Class)
(Forall (?Instance)
(=> (Instance-Of ?Instance ?Child-Class)
(Instance-Of ?Instance ?Parent-Class))))
(=>
(Forall (?Instance)
(=> (Instance-Of ?Instance ?Child-Class)
(Instance-Of ?Instance ?Parent-Class)))
(Subclass-Of ?Child-Class ?Parent-Class))
(<= (Subclass-Of ?Child-Class ?Parent-Class)
(Forall (?Instance)
(=> (Instance-Of ?Instance ?Child-Class)
(Instance-Of ?Instance ?Parent-Class))))
(<=> (Subclass-Of ?Child-Class ?Parent-Class)
(Forall (?Instance)
(=> (Instance-Of ?Instance ?Child-Class)
(Instance-Of ?Instance ?Parent-Class))))
(Nth-Argument-Name Subclass-Of 2 '?Parent-Class)
(Nth-Argument-Name Subclass-Of 1 '?Child-Class)
(<= (Subclass-Of ?Arg1 ?Arg3)
(And (Subclass-Of ?Arg1 ?Arg2) (Subclass-Of ?Arg2
?Arg3))))")
)
(make-instance [Superclass-Of] of Relation
(Arity 2)
(Documentation "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.
<H3>Notes:</H3>
<UL>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.</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Superclass-Of 2 '?Child-Class)
(Nth-Argument-Name Superclass-Of 1 '?Parent-Class))")
)
(defclass Facet "A facet is a ternary relation."
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Facet 1 '?Relation))")
(create-accessor read-write))
(single-slot Arity
(create-accessor read-write)
(default (3))
(type Integer))
)
(make-instance [Inverse] of Function
(Range Binary-Relation)
(Domain Binary-Relation)
(Arity 2)
(Function-Arity 1)
(Documentation "One binary relation is the inverse of another if they
are
equivalent when their arguments are swapped. This relation is called
SLOT-INVERSE in the OKBC 2.0 spec.
<H3>Notes:</H3>
<UL>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.originally defined in the KIF-RELATIONS
ontology</UL>" "The inverse of a binary relation is a binary relation with
all
tuples reversed.
<H3>Notes:</H3>
<UL>REDEFINED-IN-FRAME-ONTOLOGY!</UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Inverse 1 '?R)
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(=>
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation))
(= (Inverse ?Binary-Relation) ?Inverse-Relation))
(<= (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(<=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(And
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X))
(Binary-Relation ?Inverse-Relation)
(Binary-Relation ?Binary-Relation)))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(Binary-Relation ?Binary-Relation))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(Binary-Relation ?Inverse-Relation))
(=> (= (Inverse ?Binary-Relation) ?Inverse-Relation)
(<=> (Holds ?Binary-Relation ?X ?Y)
(Holds ?Inverse-Relation ?Y ?X)))
(Nth-Argument-Name Inverse 1 '?Binary-Relation))")
)
(make-instance [Domain] of Relation
(Range Class)
(Domain Slot)
(Arity 2)
(Documentation ":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.
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 <okbc-class>*) | okbc-class
An OKBC-class is any entity X for which (class X) is true or that is a
standard OKBC class described in Section 2.10.1. of the OKBC spec.
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.")
(OTHER-AXIOMS "((=> (Slot ?Slot) (Domain ?Slot Thing))
(=> (Domain ?Slot ?Class)
(=> (Template-Slot-Value ?Slot ?F ?V)
(Or (= ?F ?Class) (Subclass-Of ?F ?Class))))
(=> (Domain ?Slot ?Class)
(=> (Holds ?Slot ?F ?V) (Instance-Of ?F ?Class)))
(Nth-Argument-Name Domain 2 '?Class)
(Nth-Argument-Name Domain 1 '?Slot))")
)
(make-instance [Range] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.
This is the same as the OKBC 2.0 spec's SLOT-VALUE-TYPE, who's
documentation
reads:
: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.
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 <okbc-class>*) | (SETOF <okbc-value>*) |
okbc-class
An OKBC-class is any entity X for which (class X) is true or that is a
standard OKBC class described in Section 2.10.1. An OKBC-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 SETOF expression
allows the specification of an explicitly enumerated set of values
(e.g., either Clyde, Fred, or Robert). ")
(OTHER-AXIOMS "((=> (Range ?Relation ?Type)
(=>
(Forall (?D)
(=> (Domain ?Relation ?D) (Instance-Of ?F ?D)))
(Value-Type ?Relation ?F ?Type)))
(Nth-Argument-Name Range 2 '?Type)
(Nth-Argument-Name Range 1 '?Relation))")
)
(make-instance [Value-Type] of Relation
(Arity 3)
(Documentation "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.
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 <okbc-class>*) | (set-of <okbc-value>*) |
okbc-class
A okbc-class is any entity X for which (class X) is true or that is
a standard OKBC class described in SectionJ2.10.1. A okbc-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).")
(OTHER-AXIOMS "((=> (Value-Type ?S ?F ?C)
(=> (Template-Facet-Value Value-Type ?S ?F ?C)
(And (Class ?C)
(=> (Template-Slot-Value ?S ?F ?V) (Instance-Of ?V
?C)))))
(=> (Value-Type ?S ?F ?C)
(=> (Holds ?S ?F ?V) (Instance-Of ?V ?C)))
(Nth-Argument-Name Value-Type 3 '?C)
(Nth-Argument-Name Value-Type 2 '?F)
(Nth-Argument-Name Value-Type 1 '?S))")
)
(make-instance [Minimum-Cardinality] of Relation
(Arity 3)
(Documentation "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.
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.")
(OTHER-AXIOMS "((=> (Minimum-Cardinality ?S ?F ?N)
(>= (Set-Cardinality (Setofall ?V (Holds ?S ?F ?V))) ?N))
(Nth-Argument-Name Minimum-Cardinality 3 '?N)
(Nth-Argument-Name Minimum-Cardinality 2 '?F)
(Nth-Argument-Name Minimum-Cardinality 1 '?S))")
)
(make-instance [Cardinality] of Relation
(Arity 3)
(Documentation "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.
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.")
(OTHER-AXIOMS "((=> (Cardinality ?S ?F ?N)
(And (= ?N (Set-Cardinality (Setofall ?V (Holds ?S ?F
?V))))
(Binary-Relation ?S)))
(=>
(And (= ?N (Set-Cardinality (Setofall ?V (Holds ?S ?F
?V))))
(Binary-Relation ?S))
(Cardinality ?S ?F ?N))
(<= (Cardinality ?S ?F ?N)
(And (= ?N (Set-Cardinality (Setofall ?V (Holds ?S ?F
?V))))
(Binary-Relation ?S)))
(<=> (Cardinality ?S ?F ?N)
(And (= ?N (Set-Cardinality (Setofall ?V (Holds ?S ?F
?V))))
(Binary-Relation ?S)))
(=> (Cardinality ?S ?F ?N)
(=> (Template-Facet-Value Cardinality ?S ?F ?N)
(=
(Set-Cardinality
(Setofall ?V (Template-Slot-Value ?S ?F ?V)))
?N)))
(Binary-Relation ?S) (Nth-Argument-Name Cardinality 3 '?N)
(Nth-Argument-Name Cardinality 2 '?F)
(Nth-Argument-Name Cardinality 1 '?S))")
)
(make-instance [Maximum-Cardinality] of Relation
(Arity 3)
(Documentation "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.
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.")
(OTHER-AXIOMS "((=> (Maximum-Cardinality ?S ?F ?N)
(=> (Template-Facet-Value Maximum-Cardinality ?S ?F ?N)
(=<
(Set-Cardinality
(Setofall ?V (Template-Slot-Value ?S ?F ?V)))
?N)))
(=> (Maximum-Cardinality ?S ?F ?N)
(=< (Set-Cardinality (Setofall ?V (Holds ?S ?F ?V))) ?N))
(Nth-Argument-Name Maximum-Cardinality 3 '?N)
(Nth-Argument-Name Maximum-Cardinality 2 '?F)
(Nth-Argument-Name Maximum-Cardinality 1 '?S))")
)
(make-instance [Facet-Of] of Relation
(Arity 3)
(Documentation "From the OKBC spec:
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, OKBC 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.")
(OTHER-AXIOMS "((=> (Exists (?Value) (Holds ?Facet ?Slot ?Frame ?Value))
(Facet-Of ?Facet ?Slot ?Frame))
(Slot-Of ?Slot ?Frame) (Nth-Argument-Name Facet-Of 3
'?Frame)
(Nth-Argument-Name Facet-Of 2 '?Slot)
(Nth-Argument-Name Facet-Of 1 '?Facet))")
)
(make-instance [Template-Facet-Of] of Relation
(Arity 3)
(Documentation "From the OKBC spec:
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, OKBC 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.")
(OTHER-AXIOMS "((Template-Slot-Of ?Slot ?Class)
(=> (Template-Facet-Of ?Facet ?Slot ?Class)
(=> (Subclass-Of ?Subclass ?Class)
(Template-Facet-Of ?Facet ?Slot ?Subclass)))
(=> (Template-Facet-Of ?Facet ?Slot ?Class)
(=> (Instance-Of ?I ?Class) (Facet-Of ?Facet ?Slot ?I)))
(Nth-Argument-Name Template-Facet-Of 3 '?Class)
(Nth-Argument-Name Template-Facet-Of 2 '?Slot)
(Nth-Argument-Name Template-Facet-Of 1 '?Facet))")
)
(make-instance [Slot-Of] of Relation
(Arity 2)
(Documentation "From the OKBC spec:
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, OKBC 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.")
(OTHER-AXIOMS "((=> (Exists (?Value) (Holds ?Slot ?Frame ?Value))
(Slot-Of ?Slot ?Frame))
(Nth-Argument-Name Slot-Of 2 '?Frame)
(Nth-Argument-Name Slot-Of 1 '?Slot))")
)
(make-instance [Template-Slot-Of] of Relation
(Arity 2)
(Documentation "From the OKBC spec:
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, OKBC 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.")
(OTHER-AXIOMS "((=> (Template-Slot-Of ?Slot ?Class)
(=> (Subclass-Of ?Subclass ?Class)
(Template-Slot-Of ?Slot ?Subclass)))
(=> (Template-Slot-Of ?Slot ?Class)
(=> (Instance-Of ?I ?Class) (Slot-Of ?Slot ?I)))
(Nth-Argument-Name Template-Slot-Of 2 '?Class)
(Nth-Argument-Name Template-Slot-Of 1 '?Slot))")
)
(make-instance [Template-Slot-Value] of Relation
(Arity 3)
(Documentation "From the OKBC spec:
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)).
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.
<H3>Notes:</H3>
<UL>Obsoletes INHERITED-SLOT-VALUE</UL>")
(OTHER-AXIOMS "((Template-Slot-Of ?Slot ?Class)
(=> (Template-Slot-Value ?Slot ?Class ?Value)
(=> (Subclass-Of ?Subclass ?Class)
(Template-Slot-Value ?Slot ?Subclass ?Value)))
(=> (Template-Slot-Value ?Slot ?Class ?Value)
(=> (Instance-Of ?Instance ?Class)
(Holds ?Slot ?Instance ?Value)))
(Nth-Argument-Name Template-Slot-Value 3 '?Value)
(Nth-Argument-Name Template-Slot-Value 2 '?Class)
(Nth-Argument-Name Template-Slot-Value 1 '?Slot))")
)
(make-instance [Template-Facet-Value] of Relation
(Arity 4)
(Documentation "From the OKBC knowledge model spec:
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)).
<H3>Notes:</H3>
<UL>Obsoletes INHERITED-FACET-VALUE.</UL>")
(OTHER-AXIOMS "((Template-Facet-Of ?Facet ?Slot ?Class)
(=> (Template-Facet-Value ?Facet ?Slot ?Class ?Value)
(=> (Subclass-Of ?Subclass ?Class)
(Template-Facet-Value ?Facet ?Slot ?Subclass ?Value)))
(=> (Template-Facet-Value ?Facet ?Slot ?Class ?Value)
(=> (Instance-Of ?I ?Class) (Holds ?Facet ?Slot ?I
?Value)))
(Nth-Argument-Name Template-Facet-Value 4 '?Value)
(Nth-Argument-Name Template-Facet-Value 3 '?Class)
(Nth-Argument-Name Template-Facet-Value 2 '?Slot)
(Nth-Argument-Name Template-Facet-Value 1 '?Facet))")
)
(make-instance [Documentation-In-Frame] of Relation
(Arity 3)
(Documentation "The DOCUMENTATION-IN-FRAME facet associates a
documentation
string with a slot on a frame. It allows you to provide
documentation for polymorphic definitions.")
(OTHER-AXIOMS "((Nth-Argument-Name Documentation-In-Frame 3 '?String)
(Nth-Argument-Name Documentation-In-Frame 2 '?Slot)
(Nth-Argument-Name Documentation-In-Frame 1 '?Frame))")
)
(make-instance [Pretty-Name] of Function
(Range String)
(Arity 2)
(Function-Arity 1)
(Documentation "Indicates the string that should be used when refering
to the concept.")
(OTHER-AXIOMS "((Nth-Argument-Name Pretty-Name 1 '?Frame))")
)
(make-instance [Handle] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "Indicates the handle that should be used when referring
to the concept.")
(OTHER-AXIOMS "((Nth-Argument-Name Handle 1 '?Frame))")
)
(make-instance [Inverse-In-Frame] of Relation
(Arity 3)
(Documentation "The INVERSE-IN-FRAME 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-IN-FRAME 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.
This is the same thing as INVERSE in OKBC 2.0")
(OTHER-AXIOMS "((=> (Inverse-In-Frame ?S1 ?F ?S2)
(=> (Template-Facet-Value Inverse-In-Frame ?S1 ?F ?S2)
(And (Slot ?S2)
(=> (Template-Slot-Value ?S1 ?F ?V)
(Template-Slot-Value ?S2 ?V ?F)))))
(=> (Inverse-In-Frame ?S1 ?F ?S2)
(=> (Holds ?S1 ?F ?V) (Holds ?S2 ?V ?F)))
(Nth-Argument-Name Inverse-In-Frame 3 '?S2)
(Nth-Argument-Name Inverse-In-Frame 2 '?F)
(Nth-Argument-Name Inverse-In-Frame 1 '?S1))")
)
(make-instance [Same-Values] of Relation
(Arity 3)
(Documentation "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.
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.
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.")
(OTHER-AXIOMS "((=> (Same-Values ?S ?F (Listof @Sn))
(= (Setofall ?V (Holds ?S ?F ?V))
(Setofall ?V (Slot-Chain-Value (Listof @Sn) ?F ?V))))
(=> (Same-Values ?S1 ?F ?S2)
(= (Setofall ?V (Holds ?S1 ?F ?V))
(Setofall ?V (Holds ?S2 ?F ?V))))
(Nth-Argument-Name Same-Values 3 '?S2)
(Nth-Argument-Name Same-Values 2 '?F)
(Nth-Argument-Name Same-Values 1 '?S1))")
)
(make-instance [Slot-Chain-Value] of Relation
(Arity 3)
(Documentation "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.")
(OTHER-AXIOMS "((<=> (Slot-Chain-Value (Listof ?S) ?F ?V) (Holds ?S ?F
?V))
(<=> (Slot-Chain-Value (Listof ?S1 ?S2 @Sn) ?F ?Vn)
(Exists (?V1)
(And (Holds ?S1 ?F ?V1)
(Slot-Chain-Value (Listof ?S2 @Sn) ?V1 ?Vn))))
(Nth-Argument-Name Slot-Chain-Value 3 '?Vn)
(Nth-Argument-Name Slot-Chain-Value 2 '?F)
(Nth-Argument-Name Slot-Chain-Value 1 '?Chain))")
)
(make-instance [Not-Same-Values] of Relation
(Arity 3)
(Documentation "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.
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.")
(OTHER-AXIOMS "((=> (Not-Same-Values ?S ?F (Listof @Sn))
(Not
(= (Setofall ?V (Holds ?S ?F ?V))
(Setofall ?V (Slot-Chain-Value (Listof @Sn) ?F ?V)))))
(=> (Not-Same-Values ?S1 ?F ?S2)
(Not
(= (Setofall ?V (Holds ?S1 ?F ?V))
(Setofall ?V (Holds ?S2 ?F ?V)))))
(Nth-Argument-Name Not-Same-Values 3 '?S2)
(Nth-Argument-Name Not-Same-Values 2 '?F)
(Nth-Argument-Name Not-Same-Values 1 '?S1))")
)
(make-instance [Subset-Of-Values] of Relation
(Arity 3)
(Documentation "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.
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.")
(OTHER-AXIOMS "((=> (Subset-Of-Values ?S ?F (Listof @Sn))
(Subset (Setofall ?V (Holds ?S ?F ?V))
(Setofall ?V (Slot-Chain-Value (Listof @Sn) ?F ?V))))
(=> (Subset-Of-Values ?S1 ?F ?S2)
(Subset (Setofall ?V (Holds ?S1 ?F ?V))
(Setofall ?V (Holds ?S2 ?F ?V))))
(Nth-Argument-Name Subset-Of-Values 3 '?S2)
(Nth-Argument-Name Subset-Of-Values 2 '?F)
(Nth-Argument-Name Subset-Of-Values 1 '?S1))")
)
(make-instance [Numeric-Minimum] of Relation
(Arity 3)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Numeric-Minimum ?S ?F ?N)
(=> (Template-Facet-Value Numeric-Minimum ?S ?F ?N)
(And (Number ?N)
(=> (Template-Slot-Value ?S ?F ?V) (>= ?V ?N)))))
(=> (Numeric-Minimum ?S ?F ?N)
(=> (Holds ?S ?F ?V) (>= ?V ?N)))
(Nth-Argument-Name Numeric-Minimum 3 '?N)
(Nth-Argument-Name Numeric-Minimum 2 '?F)
(Nth-Argument-Name Numeric-Minimum 1 '?S))")
)
(make-instance [Numeric-Maximum] of Relation
(Arity 3)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Numeric-Maximum ?S ?F ?N)
(=> (Template-Facet-Value Numeric-Maximum ?S ?F ?N)
(And (Number ?N)
(=> (Template-Slot-Value ?S ?F ?V) (=< ?V ?N)))))
(=> (Numeric-Maximum ?S ?F ?N)
(=> (Holds ?S ?F ?V) (=< ?V ?N)))
(Nth-Argument-Name Numeric-Maximum 3 '?N)
(Nth-Argument-Name Numeric-Maximum 2 '?F)
(Nth-Argument-Name Numeric-Maximum 1 '?S))")
)
(make-instance [Some-Values] of Relation
(Arity 3)
(Subrelation-Of Holds)
(Documentation "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.")
(OTHER-AXIOMS "((Nth-Argument-Name Some-Values 3 '?V)
(Nth-Argument-Name Some-Values 2 '?F)
(Nth-Argument-Name Some-Values 1 '?S)
(<= (Holds @Arg-List) (Some-Values @Arg-List)))")
)
(make-instance [Collection-Type] of Relation
(Arity 3)
(Documentation "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,
OKBC
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. ")
(OTHER-AXIOMS "((Member ?V (Setof ':Set ':List ':Bag))
(Nth-Argument-Name Collection-Type 3 '?V)
(Nth-Argument-Name Collection-Type 2 '?F)
(Nth-Argument-Name Collection-Type 1 '?S))")
)
(make-instance [Slot-Not-Same-Values] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Not-Same-Values ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Not-Same-Values ?S ?F ?V)))
(Nth-Argument-Name Slot-Not-Same-Values 2 '?V)
(Nth-Argument-Name Slot-Not-Same-Values 1 '?S))")
)
(make-instance [Slot-Subset-Of-Values] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Subset-Of-Values ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Subset-Of-Values ?S ?F ?V)))
(Nth-Argument-Name Slot-Subset-Of-Values 2 '?V)
(Nth-Argument-Name Slot-Subset-Of-Values 1 '?S))")
)
(make-instance [Slot-Numeric-Minimum] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Numeric-Minimum ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Numeric-Minimum ?S ?F ?V)))
(Nth-Argument-Name Slot-Numeric-Minimum 2 '?V)
(Nth-Argument-Name Slot-Numeric-Minimum 1 '?S))")
)
(make-instance [Slot-Numeric-Maximum] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Numeric-Maximum ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Numeric-Maximum ?S ?F ?V)))
(Nth-Argument-Name Slot-Numeric-Maximum 2 '?V)
(Nth-Argument-Name Slot-Numeric-Maximum 1 '?S))")
)
(make-instance [Slot-Some-Values] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Some-Values ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Some-Values ?S ?F ?V)))
(Nth-Argument-Name Slot-Some-Values 2 '?V)
(Nth-Argument-Name Slot-Some-Values 1 '?S))")
)
(make-instance [Slot-Collection-Type] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Collection-Type ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Collection-Type ?S ?F ?V)))
(Nth-Argument-Name Slot-Collection-Type 2 '?V)
(Nth-Argument-Name Slot-Collection-Type 1 '?S))")
)
(make-instance [Slot-Cardinality] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Cardinality ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Cardinality ?S ?F ?V)))
(Nth-Argument-Name Slot-Cardinality 2 '?V)
(Nth-Argument-Name Slot-Cardinality 1 '?S))")
)
(make-instance [Slot-Maximum-Cardinality] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Maximum-Cardinality ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Maximum-Cardinality ?S ?F ?V)))
(Nth-Argument-Name Slot-Maximum-Cardinality 2 '?V)
(Nth-Argument-Name Slot-Maximum-Cardinality 1 '?S))")
)
(make-instance [Slot-Minimum-Cardinality] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Minimum-Cardinality ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Minimum-Cardinality ?S ?F ?V)))
(Nth-Argument-Name Slot-Minimum-Cardinality 2 '?V)
(Nth-Argument-Name Slot-Minimum-Cardinality 1 '?S))")
)
(make-instance [Slot-Same-Values] of Relation
(Domain Slot)
(Arity 2)
(Documentation "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.")
(OTHER-AXIOMS "((=> (Slot-Same-Values ?S ?V)
(=> (Forall (?D) (=> (Domain ?S ?D) (Instance-Of ?F ?D)))
(Same-Values ?S ?F ?V)))
(Nth-Argument-Name Slot-Same-Values 2 '?V)
(Nth-Argument-Name Slot-Same-Values 1 '?S))")
)
;;; Translation of definitions in included ontology Kif-Sets
;;; into target language Clips
(defclass Set "A set is a collection of objects, both individuals and sets
of
various sorts. It is a KIF primitive.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Set 1 '?X))")
(create-accessor read-write))
(single-slot Generalized-Intersection
(create-accessor read-write)
(type INSTANCE))
(single-slot Generalized-Union
(create-accessor read-write)
(type INSTANCE))
(single-slot Set-Cardinality
(create-accessor read-write)
(type Integer))
)
(defclass Bounded "Something is bounded if it can be a member of a set.
This is a KIF primitive.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Bounded 1 '?X))")
(create-accessor read-write))
)
(defclass Unbounded "Something in the universe of discourse that can't be a
member of a set.
Paradoxical beasts go here.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR>It would seem that the extension of this relation is empty,
since there can exist no set containing any unbounded
things.</UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Unbounded ?X) (Not (Bounded ?X)))
(=> (Not (Bounded ?X)) (Unbounded ?X))
(<= (Unbounded ?X) (Not (Bounded ?X)))
(<=> (Unbounded ?X) (Not (Bounded ?X)))
(Nth-Argument-Name Unbounded 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Class SIMPLE-SET
;;;
;;; Thing has not been included in the superset list
;;; of Simple-Set because Thing
;;; is already a superclass of Bounded.
;;;
(defclass Simple-Set "A simple set is a set that can be a member of another
set.
<H3>Notes:</H3>
<UL>The constraint that simple-set is a subclass-of thing
is specified as part of the definition of THING, but
it needs to be here, too, for bootstrapping reasons.<B>Source:
</B><A HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF
Version 3.0 Specification</A>
<BR></UL>"
(is-a Bounded Set)
(slot OTHER-AXIOMS
(default "((=> (Simple-Set ?X) (And (Bounded ?X) (Set ?X)))
(=> (And (Bounded ?X) (Set ?X)) (Simple-Set ?X))
(<= (Simple-Set ?X) (And (Bounded ?X) (Set ?X)))
(<=> (Simple-Set ?X) (And (Bounded ?X) (Set ?X)))
(=> (Simple-Set ?X) (Bounded ?X)) (=> (Simple-Set ?X) (Set
?X))
(Nth-Argument-Name Simple-Set 1 '?X))")
(create-accessor read-write))
)
(defclass Proper-Set "A proper set is a set that cannot be a member of
another set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>"
(is-a Set)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Proper-Set 1 '?X))")
(create-accessor read-write))
)
(make-instance [Member] of Relation
(Range Set)
(Domain Bounded)
(Arity 2)
(Documentation "The sentence {tt (member $tau_1$ $tau_2$)} is true if
and only if the
object denoted by $tau_1$ is contained in the set denoted by $tau_2$.
As mentioned above, an object can be a member of another object if and only
if the former is bounded and the latter is a set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Member 2 '?Set)
(Nth-Argument-Name Member 1 '?Element))")
)
(make-instance [Extensionality-Property-Of-Sets] of Named-Axiom
(Documentation "Two sets are identical if and only if they have the same
members.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((=> (And (Set ?S1) (Set ?S2))
(<=>
(Forall (?X)
(<=> (Member ?X ?S1) (Member ?X ?S2)))
(= ?S1 ?S2))))")
)
(defclass Empty "True of the empty set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Empty ?X) (= ?X (Setof))) (=> (= ?X (Setof)) (Empty ?X))
(<= (Empty ?X) (= ?X (Setof))) (<=> (Empty ?X) (= ?X
(Setof)))
(Nth-Argument-Name Empty 1 '?X))")
(create-accessor read-write))
)
(make-instance [Union] of Function
(Range Set)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Union @Sets) ?Set)
(=> (Item ?S (Listof @Sets)) (Set ?S)))
(Undefined (Arity Union)) (Undefined (Function-Arity
Union)))")
)
(make-instance [Intersection] of Function
(Range Set)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Intersection @Sets) ?Set)
(=> (Item ?S (Listof @Sets)) (Set ?S)))
(Undefined (Arity Intersection))
(Undefined (Function-Arity Intersection)))")
)
(make-instance [Difference] of Function
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Difference ?Set @Sets) ?Diff-Set)
(=> (Item ?S (Listof @Sets)) (Set ?S)))
(Undefined (Arity Difference))
(Undefined (Function-Arity Difference))
(Nth-Argument-Name Difference 1 '?Set))")
)
(make-instance [Complement] of Function
(Range Set)
(Domain Set)
(Arity 2)
(Function-Arity 1)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((Nth-Argument-Name Complement 1 '?S))")
)
(make-instance [Generalized-Union] of Function
(Range Set)
(Domain Set)
(Arity 2)
(Function-Arity 1)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Generalized-Union ?Set-Of-Sets) ?Set)
(Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set
?S))))
(Nth-Argument-Name Generalized-Union 1 '?Set-Of-Sets))")
)
(make-instance [Generalized-Intersection] of Function
(Range Set)
(Domain Set)
(Arity 2)
(Function-Arity 1)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (= (Generalized-Intersection ?Set-Of-Sets) ?Set)
(Forall (?S) (=> (Member ?S ?Set-Of-Sets) (Simple-Set
?S))))
(Nth-Argument-Name Generalized-Intersection 1
'?Set-Of-Sets))")
)
(make-instance [Subset] of Relation
(Arity 2)
(Range Set)
(Domain Set)
(Documentation "The sentence {tt (subset $tau_1$ $tau_2$)} is true if
and only if $tau_1$ and $tau_2$ are sets and the objects in the set
denoted by $tau_1$ are contained in the set denoted by $tau_2$.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Subset ?S1 ?S2)
(And (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2)))
(Set ?S2) (Set ?S1)))
(=>
(And (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2)))
(Set ?S2) (Set ?S1))
(Subset ?S1 ?S2))
(<= (Subset ?S1 ?S2)
(And (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2)))
(Set ?S2) (Set ?S1)))
(<=> (Subset ?S1 ?S2)
(And (Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2)))
(Set ?S2) (Set ?S1)))
(=> (Subset ?S1 ?S2)
(Forall (?X) (=> (Member ?X ?S1) (Member ?X ?S2))))
(Set ?S2) (Set ?S1) (Nth-Argument-Name Subset 2 '?S2)
(Nth-Argument-Name Subset 1 '?S1))")
)
(make-instance [Proper-Subset] of Relation
(Arity 2)
(Subrelation-Of Subset)
(Documentation "The sentence {tt (proper-subset $tau_1$ $tau_2$)} is
true if
the set denoted by $tau_1$ is a subset of the set denoted by $tau_2$
but not vice-versa.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Proper-Subset ?S1 ?S2)
(And (Not (Subset ?S2 ?S1)) (Subset ?S1 ?S2)))
(=> (And (Not (Subset ?S2 ?S1)) (Subset ?S1 ?S2))
(Proper-Subset ?S1 ?S2))
(<= (Proper-Subset ?S1 ?S2)
(And (Not (Subset ?S2 ?S1)) (Subset ?S1 ?S2)))
(<=> (Proper-Subset ?S1 ?S2)
(And (Not (Subset ?S2 ?S1)) (Subset ?S1 ?S2)))
(=> (Proper-Subset ?S1 ?S2) (Not (Subset ?S2 ?S1)))
(=> (Proper-Subset ?S1 ?S2) (Subset ?S1 ?S2))
(Nth-Argument-Name Proper-Subset 2 '?S2)
(Nth-Argument-Name Proper-Subset 1 '?S1)
(<= (Subset @Arg-List) (Proper-Subset @Arg-List)))")
)
(make-instance [Disjoint] of Relation
(Arity 2)
(Documentation "Two sets are disjoint if and only if there is no object
that is a
member of both sets.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))
(=> (Empty (Intersection ?S1 ?S2)) (Disjoint ?S1 ?S2))
(<= (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))
(<=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))
(Nth-Argument-Name Disjoint 2 '?S2)
(Nth-Argument-Name Disjoint 1 '?S1))")
)
(make-instance [Pairwise-Disjoint] of Relation
(Documentation "Sets are pairwise-disjoint if and only if every
set is disjoint from every other set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Pairwise-Disjoint @Sets)
(Forall (?S1 ?S2)
(=> (Item ?S1 (Listof @Sets)) (Item ?S2 (Listof @Sets))
(Or (= ?S1 ?S2) (Disjoint ?S1 ?S2)))))
(=>
(Forall (?S1 ?S2)
(=> (Item ?S1 (Listof @Sets)) (Item ?S2 (Listof @Sets))
(Or (= ?S1 ?S2) (Disjoint ?S1 ?S2))))
(Pairwise-Disjoint @Sets))
(<= (Pairwise-Disjoint @Sets)
(Forall (?S1 ?S2)
(=> (Item ?S1 (Listof @Sets)) (Item ?S2 (Listof @Sets))
(Or (= ?S1 ?S2) (Disjoint ?S1 ?S2)))))
(<=> (Pairwise-Disjoint @Sets)
(Forall (?S1 ?S2)
(=> (Item ?S1 (Listof @Sets)) (Item ?S2 (Listof @Sets))
(Or (= ?S1 ?S2) (Disjoint ?S1 ?S2)))))
(Undefined (Arity Pairwise-Disjoint))
(Nth-Argument-Name Pairwise-Disjoint 1 '@Sets))")
)
(make-instance [Mutually-Disjoint] of Relation
(Documentation "Sets are mutually-disjoint if and only if there is no
object that
is a member of all of the sets.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Mutually-Disjoint @Sets) (Empty (Intersection
@Sets)))
(=> (Empty (Intersection @Sets)) (Mutually-Disjoint
@Sets))
(<= (Mutually-Disjoint @Sets) (Empty (Intersection
@Sets)))
(<=> (Mutually-Disjoint @Sets) (Empty (Intersection
@Sets)))
(Undefined (Arity Mutually-Disjoint))
(Nth-Argument-Name Mutually-Disjoint 1 '@Sets))")
)
(make-instance [Set-Partition] of Relation
(Range Pairwise-Disjoint)
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Set-Partition ?S @Sets)
(And (Pairwise-Disjoint @Sets) (= ?S (Union @Sets))))
(=> (And (Pairwise-Disjoint @Sets) (= ?S (Union @Sets)))
(Set-Partition ?S @Sets))
(<= (Set-Partition ?S @Sets)
(And (Pairwise-Disjoint @Sets) (= ?S (Union @Sets))))
(<=> (Set-Partition ?S @Sets)
(And (Pairwise-Disjoint @Sets) (= ?S (Union @Sets))))
(Undefined (Arity Set-Partition)) (Pairwise-Disjoint
@Sets)
(Nth-Argument-Name Set-Partition 2 '@Sets)
(Nth-Argument-Name Set-Partition 1 '?S))")
)
(make-instance [Set-Cover] of Relation
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>")
(OTHER-AXIOMS "((=> (Set-Cover ?S @Sets) (Subset ?S (Union @Sets)))
(=> (Subset ?S (Union @Sets)) (Set-Cover ?S @Sets))
(<= (Set-Cover ?S @Sets) (Subset ?S (Union @Sets)))
(<=> (Set-Cover ?S @Sets) (Subset ?S (Union @Sets)))
(Undefined (Arity Set-Cover))
(Nth-Argument-Name Set-Cover 2 '@Sets)
(Nth-Argument-Name Set-Cover 1 '?S))")
)
(make-instance [Axiom-Of-Regularity] of Named-Axiom
(Documentation "every non-empty set has an element with which it has no
members in
common.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((Forall (?S)
(=> (Not (Empty ?S))
(Exists (?U)
(And (Member ?U ?S) (Disjoint ?U ?S))))))")
)
(make-instance [Axiom-Of-Choice] of Named-Axiom
(Documentation "There is a set that associates every bounded set with a
distinguished element of that set. In effect, it {it chooses} an
element from every bounded set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((Exists (?S)
(And (Set ?S)
(Forall (?X) (=> (Member ?X ?S) (Double
?X)))
(Forall (?X ?Y ?Z)
(=>
(And (Member (Listof ?X ?Y) ?S)
(Member (Listof ?X ?Z) ?S))
(= ?Y ?Z)))
(Forall (?U)
(=> (And (Bounded ?U) (Not (Empty ?U)))
(Exists (?V)
(And (Member ?V ?U)
(Member (Listof ?U ?V) ?S))))))))")
)
(make-instance [Finite-Set-Axiom] of Named-Axiom
(Documentation "Any finite set of bounded sets is itself a bounded set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((=> (Finite-Set ?S) (Bounded ?S)))")
)
(make-instance [Subset-Axiom] of Named-Axiom
(Documentation "The set of all of subsets of a bounded set is also a
bounded set.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((=> (Bounded ?V)
(Bounded (Setofall ?U (Subset ?U ?V)))))")
)
(make-instance [Union-Axiom] of Named-Axiom
(Documentation "
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((=>
(And (Bounded ?U)
(Forall (?X) (=> (Member ?X ?U) (Bounded
?X))))
(Bounded (Generalized-Union ?U))))")
)
(make-instance [Intersection-Axiom] of Named-Axiom
(Documentation "The intersection of a bounded set and any other set is a
bounded
set. So long as one of the sets defining the intersection is bounded,
the resulting set is bounded.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((=> (And (Bounded ?U) (Set ?S))
(Bounded (Intersection ?U ?S))))")
)
(make-instance [Axiom-Of-Infinity] of Named-Axiom
(Documentation "There is a bounded set containing a set, a set that
properly
contains that set, a third set that properly contains the second set,
and so forth. In short, there is at least one bounded set of infinite
cardinality.
<H3>Notes:</H3>
<UL><B>Source: </B><A
HREF=\"http://www-ksl.stanford.edu/knowledge-sharing/kif/\">KIF Version 3.0
Specification</A>
<BR></UL>") (OTHER-AXIOMS "((Exists (?U)
(And (Bounded ?U) (Not (Empty ?U))
(Forall (?X)
(=> (Member ?X ?U)
(Exists (?Y)
(And (Member ?Y ?U)
(Proper-Subset ?X ?Y))))))))")
)
;;; --- In the definition of Instance TRUE
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance FALSE
;;;
;;; Unknown construct in CLIPS.
;;;
;;; Translation of definitions in included ontology Kif-Lists
;;; into target language Clips
(defclass List "A list is a sequence --- an ordered bag --- of elements.
It is KIF primitive."
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name List 1 '?X))")
(create-accessor read-write))
(single-slot Reverse
(create-accessor read-write)
(type INSTANCE))
(single-slot Last
(create-accessor read-write))
)
(defclass Null "True of the list with no items."
(is-a List)
(slot OTHER-AXIOMS
(default "((=> (Null ?List) (And (= (Length ?List) 0) (List ?List)))
(=> (And (= (Length ?List) 0) (List ?List)) (Null ?List))
(<= (Null ?List) (And (= (Length ?List) 0) (List ?List)))
(<=> (Null ?List) (And (= (Length ?List) 0) (List ?List)))
(=> (Null ?List) (List ?List)) (Nth-Argument-Name Null 1
'?List))")
(create-accessor read-write))
)
;;; --- In the definition of Instance NIL
;;;
;;; Unknown construct in CLIPS.
;;;
(defclass Single "A list of length 1."
(is-a List)
(slot OTHER-AXIOMS
(default "((=> (Single ?List) (And (= (Length ?List) 1) (List ?List)))
(=> (And (= (Length ?List) 1) (List ?List)) (Single ?List))
(<= (Single ?List) (And (= (Length ?List) 1) (List ?List)))
(<=> (Single ?List) (And (= (Length ?List) 1) (List ?List)))
(=> (Single ?List) (List ?List))
(Nth-Argument-Name Single 1 '?List))")
(create-accessor read-write))
)
(defclass Double "A list of length 2."
(is-a List)
(slot OTHER-AXIOMS
(default "((=> (Double ?List) (And (= (Length ?List) 2) (List ?List)))
(=> (And (= (Length ?List) 2) (List ?List)) (Double ?List))
(<= (Double ?List) (And (= (Length ?List) 2) (List ?List)))
(<=> (Double ?List) (And (= (Length ?List) 2) (List ?List)))
(=> (Double ?List) (List ?List))
(Nth-Argument-Name Double 1 '?List))")
(create-accessor read-write))
)
(defclass Triple "A list of length 3."
(is-a List)
(slot OTHER-AXIOMS
(default "((=> (Triple ?List) (And (= (Length ?List) 3) (List ?List)))
(=> (And (= (Length ?List) 3) (List ?List)) (Triple ?List))
(<= (Triple ?List) (And (= (Length ?List) 3) (List ?List)))
(<=> (Triple ?List) (And (= (Length ?List) 3) (List ?List)))
(=> (Triple ?List) (List ?List))
(Nth-Argument-Name Triple 1 '?List))")
(create-accessor read-write))
)
(make-instance [First] of Function
(Domain List)
(Arity 2)
(Function-Arity 1)
(OTHER-AXIOMS "((Nth-Argument-Name First 1 '?List))")
)
(make-instance [Rest] of Function
(Arity 2)
(Function-Arity 1)
(OTHER-AXIOMS "((=>
(Or (And (Null ?List) (= ?Rest-List ?List))
(Exists (?X @Items)
(And (= ?List (Listof ?X @Items))
(= ?Rest-List (Listof @Items)))))
(= (Rest ?List) ?Rest-List))
(<= (= (Rest ?List) ?Rest-List)
(Or (And (Null ?List) (= ?Rest-List ?List))
(Exists (?X @Items)
(And (= ?List (Listof ?X @Items))
(= ?Rest-List (Listof @Items))))))
(<=> (= (Rest ?List) ?Rest-List)
(Or (And (Null ?List) (= ?Rest-List ?List))
(Exists (?X @Items)
(And (= ?List (Listof ?X @Items))
(= ?Rest-List (Listof @Items))))))
(=> (= (Rest ?List) ?Rest-List)
(Or (And (Null ?List) (= ?Rest-List ?List))
(Exists (?X @Items)
(And (= ?List (Listof ?X @Items))
(= ?Rest-List (Listof @Items))))))
(Nth-Argument-Name Rest 1 '?List))")
)
(make-instance [Last] of Function
(Domain List)
(Arity 2)
(Function-Arity 1)
(OTHER-AXIOMS "((Nth-Argument-Name Last 1 '?List))")
)
(make-instance [Butlast] of Function
(Arity 2)
(Function-Arity 1)
(OTHER-AXIOMS "((Nth-Argument-Name Butlast 1 '?List))")
)
(make-instance [Item] of Relation
(Range List)
(Arity 2)
(Documentation "The sentence {tt (item $tau_1$ $tau_2$)} is true if and
only if
the object denoted by $tau_2$ is a non-empty list and the object
denoted by $tau_1$ is either the first item of that list or an item in
the rest of the list.")
(OTHER-AXIOMS "((=> (Item ?X ?List)
(Or (= ?X (First ?List)) (Item ?X (Rest ?List))))
(Not (Null ?List)) (Nth-Argument-Name Item 2 '?List)
(Nth-Argument-Name Item 1 '?X))")
)
(make-instance [Sublist] of Relation
(Range List)
(Domain List)
(Arity 2)
(Documentation "The sentence {tt (sublist $tau_1$ $tau_2$)} is true if
and only if
the object denoted by $tau_1$ is a final segment of the list denoted by
$tau_2$.")
(OTHER-AXIOMS "((=> (Sublist ?L1 ?L2)
(Or (= ?L1 ?L2) (Sublist ?L1 (Rest ?L2))))
(Nth-Argument-Name Sublist 2 '?L2)
(Nth-Argument-Name Sublist 1 '?L1))")
)
(make-instance [Cons] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The function {tt cons} adds the object specified as its
first
argument to the front of the list specified as its second argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Cons 2 '?List)
(Nth-Argument-Name Cons 1 '?X))")
)
(make-instance [Append] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The function {tt append} adds the items in the list
specified as its first
argument to the list specified as its second argument. .")
(OTHER-AXIOMS "((Nth-Argument-Name Append 2 '?L2)
(Nth-Argument-Name Append 1 '?L1))")
)
(make-instance [Revappend] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The function {tt revappend} is similar to append, except
that it
adds the items in reverse order.")
(OTHER-AXIOMS "((Nth-Argument-Name Revappend 2 '?L2)
(Nth-Argument-Name Revappend 1 '?L1))")
)
(make-instance [Reverse] of Function
(Range List)
(Domain List)
(Arity 2)
(Function-Arity 1)
(Documentation "The function {tt reverse} produces a list in which the
order of items is the
reverse of that in the list supplied as its single argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Reverse 1 '?List))")
)
(make-instance [Adjoin] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The functions {tt adjoin} and {tt remove} construct
lists by adding or
removing objects from the lists specified as their arguments.")
(OTHER-AXIOMS "((Nth-Argument-Name Adjoin 2 '?List)
(Nth-Argument-Name Adjoin 1 '?X))")
)
(make-instance [Remove] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "The functions {tt adjoin} and {tt remove} construct
lists by adding or
removing objects from the lists specified as their arguments.")
(OTHER-AXIOMS "((Nth-Argument-Name Remove 2 '?List)
(Nth-Argument-Name Remove 1 '?X))")
)
(make-instance [Subst] of Function
(Arity 4)
(Function-Arity 3)
(Documentation "The value of {tt subst} is the object or list obtained
by
substituting the object supplied as first argument for all occurrences
of the object supplied as second argument in the object or list
supplied as third argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Subst 3 '?Z)
(Nth-Argument-Name Subst 2 '?Y)
(Nth-Argument-Name Subst 1 '?X))")
)
(make-instance [Length] of Function
(Range Nonnegative-Integer)
(Domain List)
(Arity 2)
(Function-Arity 1)
(Documentation "The function constant {tt length} gives the number of
items in a list.")
(OTHER-AXIOMS "((Nth-Argument-Name Length 1 '?List))")
)
(make-instance [Nth] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "{tt nth} returns the item in the list specified as its
first
argument in the position specified as its second argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Nth 2 '?N)
(Nth-Argument-Name Nth 1 '?List))")
)
(make-instance [Nthrest] of Function
(Arity 3)
(Function-Arity 2)
(Documentation "{tt nthrest} returns the list specified as its first
argument
minus the first $n$ items, where $n$ is the number specified as its
second argument.")
(OTHER-AXIOMS "((Nth-Argument-Name Nthrest 2 '?N)
(Nth-Argument-Name Nthrest 1 '?List))")
)
;;; Translation of definitions in included ontology Kif-Meta
;;; into target language Clips
(defclass Expression "KIF expression is either a word or a list of
expressions."
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Expression ?Expr)
(Or (Word ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr) (Expression ?Subexpr))))))
(=>
(Or (Word ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr) (Expression ?Subexpr)))))
(Expression ?Expr))
(<= (Expression ?Expr)
(Or (Word ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr) (Expression ?Subexpr))))))
(<=> (Expression ?Expr)
(Or (Word ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr) (Expression ?Subexpr))))))
(Nth-Argument-Name Expression 1 '?Expr))")
(create-accessor read-write))
)
(defclass Word "An atom in a KIF expression.
<H3>Notes:</H3>
<UL>Word used to be partitioned into variable, constant, and OPERATOR,
but examination of p.8 of the spec reveals that operators are
not
words, which is a relief because this was causing exhaustive-
subclass partition barfage because variable and constant were
both members of the partitions of Word and Term. Term has been
updated so as to be partitioned into Word and the non-atomic
terms. JPR.
<BR></UL>"
(is-a Expression)
(slot OTHER-AXIOMS
(default "((=> (Word ?Expr) (Not (List ?Expr)))
(Nth-Argument-Name Word 1 '?Expr))")
(create-accessor read-write))
)
(defclass Variable "KIF variable"
(is-a Word)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Variable 1 '?Expr))")
(create-accessor read-write))
)
(defclass Operator "KIF operator"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=> (Operator ?Expr) (Not (List ?Expr)))
(Nth-Argument-Name Operator 1 '?Expr))")
(create-accessor read-write))
)
(defclass Constant "A constant used in a KIF expression."
(is-a Word)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Constant 1 '?Expr))")
(create-accessor read-write))
(multislot Defining-Axiom
(create-accessor read-write)
(type INSTANCE))
)
(defclass Funconst "A symbol that denotes a function. Used as the functor
of a
term expression."
(is-a Constant)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Funconst 1 '?Symbol))")
(create-accessor read-write))
)
(defclass Relconst "A symbol that denotes a relation (may also be a
function).
Cannot be used as a functor of a term expression, even if it denotes
a function."
(is-a Constant)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Relconst 1 '?Symbol))")
(create-accessor read-write))
)
(defclass Objconst "A symbol that denotes a KIF object other than a
relation."
(is-a Constant)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Objconst 1 '?Symbol))")
(create-accessor read-write))
)
(defclass Indvar "An individual variable in a KIF expression.
For every individual variable $nu$, there is an axiom asserting that it is
indeed an individual variable. Each such axiom is a defining axiom for the
{tt indvar} relation."
(is-a Variable)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Indvar 1 '?Expression))")
(create-accessor read-write))
)
(defclass Seqvar "A sequence variable in a KIF expression.
For every sequence variable $omega$, there is an axiom asserting that it is
a
sequence variable. Each such axiom is a defining axiom for the {tt seqvar}
relation."
(is-a Variable)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Seqvar 1 '?Expression))")
(create-accessor read-write))
)
(defclass Termop "KIF term operator"
(is-a Operator)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Termop 1 '?Expr))")
(create-accessor read-write))
)
(defclass Sentop "KIF sentence operator"
(is-a Operator)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Sentop 1 '?Expr))")
(create-accessor read-write))
)
(defclass Ruleop "KIF rule operator"
(is-a Operator)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Ruleop 1 '?Expr))")
(create-accessor read-write))
)
(defclass Defop "KIF definitional operator"
(is-a Operator)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Defop 1 '?Expr))")
(create-accessor read-write))
)
(defclass Term "KIF term expression
<H3>Notes:</H3>
<UL>See notes on Word.
<BR></UL>"
(is-a Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Term 1 '?Expr))")
(create-accessor read-write))
)
(defclass Funterm "KIF function term expression."
(is-a List Term)
(slot OTHER-AXIOMS
(default "((=> (Funterm ?Expr)
(And (Value-Type First ?Expr Funconst)
(Cardinality First ?Expr 1) (List ?Expr) (Term ?Expr)))
(=>
(And (Value-Type First ?Expr Funconst)
(Cardinality First ?Expr 1) (List ?Expr) (Term ?Expr))
(Funterm ?Expr))
(<= (Funterm ?Expr)
(And (Value-Type First ?Expr Funconst)
(Cardinality First ?Expr 1) (List ?Expr) (Term ?Expr)))
(<=> (Funterm ?Expr)
(And (Value-Type First ?Expr Funconst)
(Cardinality First ?Expr 1) (List ?Expr) (Term ?Expr)))
(=> (Funterm ?Expr) (Value-Type First ?Expr Funconst))
(=> (Funterm ?Expr) (Cardinality First ?Expr 1))
(=> (Funterm ?Expr) (List ?Expr))
(=> (Funterm ?Expr) (Term ?Expr))
(Nth-Argument-Name Funterm 1 '?Expr))")
(create-accessor read-write))
)
(defclass Listterm "KIF list term expression"
(is-a List Term)
(slot OTHER-AXIOMS
(default "((=> (Listterm ?Expr)
(And (= (First ?Expr) 'Listof) (List ?Expr) (Term ?Expr)))
(=> (And (= (First ?Expr) 'Listof) (List ?Expr) (Term ?Expr))
(Listterm ?Expr))
(<= (Listterm ?Expr)
(And (= (First ?Expr) 'Listof) (List ?Expr) (Term ?Expr)))
(<=> (Listterm ?Expr)
(And (= (First ?Expr) 'Listof) (List ?Expr) (Term ?Expr)))
(=> (Listterm ?Expr) (= (First ?Expr) 'Listof))
(=> (Listterm ?Expr) (List ?Expr))
(=> (Listterm ?Expr) (Term ?Expr))
(Nth-Argument-Name Listterm 1 '?Expr))")
(create-accessor read-write))
)
(defclass Setterm "KIF set term expression"
(is-a List Term)
(slot OTHER-AXIOMS
(default "((=> (Setterm ?Expr)
(And (= (First ?Expr) 'Setof) (List ?Expr) (Term ?Expr)))
(=> (And (= (First ?Expr) 'Setof) (List ?Expr) (Term ?Expr))
(Setterm ?Expr))
(<= (Setterm ?Expr)
(And (= (First ?Expr) 'Setof) (List ?Expr) (Term ?Expr)))
(<=> (Setterm ?Expr)
(And (= (First ?Expr) 'Setof) (List ?Expr) (Term ?Expr)))
(=> (Setterm ?Expr) (= (First ?Expr) 'Setof))
(=> (Setterm ?Expr) (List ?Expr))
(=> (Setterm ?Expr) (Term ?Expr))
(Nth-Argument-Name Setterm 1 '?Expr))")
(create-accessor read-write))
)
(defclass Quoterm "KIF quoted term expression."
(is-a List Term)
(slot OTHER-AXIOMS
(default "((=> (Quoterm ?Expr)
(And (Expression (First (First ?Expr)))
(= (First ?Expr) 'Quote) (List ?Expr) (Term ?Expr)))
(=>
(And (Expression (First (First ?Expr)))
(= (First ?Expr) 'Quote) (List ?Expr) (Term ?Expr))
(Quoterm ?Expr))
(<= (Quoterm ?Expr)
(And (Expression (First (First ?Expr)))
(= (First ?Expr) 'Quote) (List ?Expr) (Term ?Expr)))
(<=> (Quoterm ?Expr)
(And (Expression (First (First ?Expr)))
(= (First ?Expr) 'Quote) (List ?Expr) (Term ?Expr)))
(=> (Quoterm ?Expr) (Expression (First (First ?Expr))))
(=> (Quoterm ?Expr) (= (First ?Expr) 'Quote))
(=> (Quoterm ?Expr) (List ?Expr))
(=> (Quoterm ?Expr) (Term ?Expr))
(Nth-Argument-Name Quoterm 1 '?Expr))")
(create-accessor read-write))
)
(defclass Logterm
(is-a Term)
(slot OTHER-AXIOMS
(default "((=> (Logterm ?X)
(Or
(Exists (?P1 ?T1)
(And (Sentence ?P1) (Term ?T1) (= ?X (Listof 'If ?P1
?T1))))
(Exists (?P1 ?T1 ?T2)
(And (Sentence ?P1) (Term ?T1) (Term ?T2)
(= ?X (Listof 'If ?P1 ?T1 ?T2))))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence ?P) (Term ?T) (= ?C (Listof ?P ?T)))))
(= ?X (Cons 'Cond ?Clist))))))
(=>
(Or
(Exists (?P1 ?T1)
(And (Sentence ?P1) (Term ?T1) (= ?X (Listof 'If ?P1
?T1))))
(Exists (?P1 ?T1 ?T2)
(And (Sentence ?P1) (Term ?T1) (Term ?T2)
(= ?X (Listof 'If ?P1 ?T1 ?T2))))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence ?P) (Term ?T) (= ?C (Listof ?P ?T)))))
(= ?X (Cons 'Cond ?Clist)))))
(Logterm ?X))
(<= (Logterm ?X)
(Or
(Exists (?P1 ?T1)
(And (Sentence ?P1) (Term ?T1) (= ?X (Listof 'If ?P1
?T1))))
(Exists (?P1 ?T1 ?T2)
(And (Sentence ?P1) (Term ?T1) (Term ?T2)
(= ?X (Listof 'If ?P1 ?T1 ?T2))))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence ?P) (Term ?T) (= ?C (Listof ?P ?T)))))
(= ?X (Cons 'Cond ?Clist))))))
(<=> (Logterm ?X)
(Or
(Exists (?P1 ?T1)
(And (Sentence ?P1) (Term ?T1) (= ?X (Listof 'If ?P1
?T1))))
(Exists (?P1 ?T1 ?T2)
(And (Sentence ?P1) (Term ?T1) (Term ?T2)
(= ?X (Listof 'If ?P1 ?T1 ?T2))))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence ?P) (Term ?T) (= ?C (Listof ?P ?T)))))
(= ?X (Cons 'Cond ?Clist))))))
(Nth-Argument-Name Logterm 1 '?X))")
(create-accessor read-write))
)
(defclass Quanterm
(is-a Term)
(slot OTHER-AXIOMS
(default "((=> (Quanterm ?X)
(Or
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P) (= ?X (Listof 'The ?T ?P))))
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P)
(= ?X (Listof 'Setofall ?T ?P))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?P)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Kappa (Append ?Vlist (Listof ?Sv)) ?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist) (Term ?T) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?T)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Lambda (Append ?Vlist (Listof ?Sv))
?T))))))
(=>
(Or
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P) (= ?X (Listof 'The ?T ?P))))
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P)
(= ?X (Listof 'Setofall ?T ?P))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?P)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Kappa (Append ?Vlist (Listof ?Sv)) ?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist) (Term ?T) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?T)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Lambda (Append ?Vlist (Listof ?Sv))
?T)))))
(Quanterm ?X))
(<= (Quanterm ?X)
(Or
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P) (= ?X (Listof 'The ?T ?P))))
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P)
(= ?X (Listof 'Setofall ?T ?P))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?P)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Kappa (Append ?Vlist (Listof ?Sv)) ?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist) (Term ?T) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?T)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Lambda (Append ?Vlist (Listof ?Sv))
?T))))))
(<=> (Quanterm ?X)
(Or
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P) (= ?X (Listof 'The ?T ?P))))
(Exists (?T ?P)
(And (Term ?T) (Sentence ?P)
(= ?X (Listof 'Setofall ?T ?P))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?P)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Kappa (Append ?Vlist (Listof ?Sv)) ?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist) (Term ?T) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist) (Seqvar ?Sv) (Sentence ?T)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X (Listof 'Lambda (Append ?Vlist (Listof ?Sv))
?T))))))
(Nth-Argument-Name Quanterm 1 '?X))")
(create-accessor read-write))
)
(defclass Sentence "KIF sentence expression. Has a truth value."
(is-a Expression)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Sentence 1 '?Expr))")
(create-accessor read-write))
)
(defclass Logconst "A KIF logical constant."
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Logconst 1 '?X))")
(create-accessor read-write))
)
(defclass Relsent
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((=> (Relsent ?X)
(Exists (?R ?Tlist)
(And (Or (Relconst ?R) (Funconst ?R)) (List ?Tlist)
(>= (Length ?Tlist) 1) (=> (Item ?T ?Tlist) (Term ?T))
(= ?X (Cons ?R ?Tlist)))))
(=>
(Exists (?R ?Tlist)
(And (Or (Relconst ?R) (Funconst ?R)) (List ?Tlist)
(>= (Length ?Tlist) 1) (=> (Item ?T ?Tlist) (Term ?T))
(= ?X (Cons ?R ?Tlist))))
(Relsent ?X))
(<= (Relsent ?X)
(Exists (?R ?Tlist)
(And (Or (Relconst ?R) (Funconst ?R)) (List ?Tlist)
(>= (Length ?Tlist) 1) (=> (Item ?T ?Tlist) (Term ?T))
(= ?X (Cons ?R ?Tlist)))))
(<=> (Relsent ?X)
(Exists (?R ?Tlist)
(And (Or (Relconst ?R) (Funconst ?R)) (List ?Tlist)
(>= (Length ?Tlist) 1) (=> (Item ?T ?Tlist) (Term ?T))
(= ?X (Cons ?R ?Tlist)))))
(Nth-Argument-Name Relsent 1 '?X))")
(create-accessor read-write))
)
(defclass Equation
(is-a Relsent)
(slot OTHER-AXIOMS
(default "((=> (Equation ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '= ?T1 ?T2))))
(Relsent ?X)))
(=>
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '= ?T1 ?T2))))
(Relsent ?X))
(Equation ?X))
(<= (Equation ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '= ?T1 ?T2))))
(Relsent ?X)))
(<=> (Equation ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '= ?T1 ?T2))))
(Relsent ?X)))
(=> (Equation ?X)
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '= ?T1 ?T2)))))
(=> (Equation ?X) (Relsent ?X))
(Nth-Argument-Name Equation 1 '?X))")
(create-accessor read-write))
)
(defclass Inequality
(is-a Relsent)
(slot OTHER-AXIOMS
(default "((=> (Inequality ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '/= ?T1 ?T2))))
(Relsent ?X)))
(=>
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '/= ?T1 ?T2))))
(Relsent ?X))
(Inequality ?X))
(<= (Inequality ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '/= ?T1 ?T2))))
(Relsent ?X)))
(<=> (Inequality ?X)
(And
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '/= ?T1 ?T2))))
(Relsent ?X)))
(=> (Inequality ?X)
(Exists (?T1 ?T2)
(And (Term ?T1) (Term ?T2) (= ?X (Listof '/= ?T1 ?T2)))))
(=> (Inequality ?X) (Relsent ?X))
(Nth-Argument-Name Inequality 1 '?X))")
(create-accessor read-write))
)
(defclass Logsent "KIF logical sentence."
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Logsent 1 '?Expr))")
(create-accessor read-write))
)
(defclass Negation
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Negation ?X)
(Exists (?P) (And (Sentence ?P) (= ?X (Listof 'Not ?P)))))
(=> (Exists (?P) (And (Sentence ?P) (= ?X (Listof 'Not ?P))))
(Negation ?X))
(<= (Negation ?X)
(Exists (?P) (And (Sentence ?P) (= ?X (Listof 'Not ?P)))))
(<=> (Negation ?X)
(Exists (?P) (And (Sentence ?P) (= ?X (Listof 'Not ?P)))))
(Nth-Argument-Name Negation 1 '?X))")
(create-accessor read-write))
)
(defclass Conjunction
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Conjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'And ?Plist)))))
(=>
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'And ?Plist))))
(Conjunction ?X))
(<= (Conjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'And ?Plist)))))
(<=> (Conjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'And ?Plist)))))
(Nth-Argument-Name Conjunction 1 '?X))")
(create-accessor read-write))
)
(defclass Disjunction
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Disjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'Or ?Plist)))))
(=>
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'Or ?Plist))))
(Disjunction ?X))
(<= (Disjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'Or ?Plist)))))
(<=> (Disjunction ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons 'Or ?Plist)))))
(Nth-Argument-Name Disjunction 1 '?X))")
(create-accessor read-write))
)
(defclass Implication
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '=> ?Plist)))))
(=>
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '=> ?Plist))))
(Implication ?X))
(<= (Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '=> ?Plist)))))
(<=> (Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '=> ?Plist)))))
(Nth-Argument-Name Implication 1 '?X))")
(create-accessor read-write))
)
(defclass Reverse-Implication
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Reverse-Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '<= ?Plist)))))
(=>
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '<= ?Plist))))
(Reverse-Implication ?X))
(<= (Reverse-Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '<= ?Plist)))))
(<=> (Reverse-Implication ?X)
(Exists (?Plist)
(And (List ?Plist) (>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons '<= ?Plist)))))
(Nth-Argument-Name Reverse-Implication 1 '?X))")
(create-accessor read-write))
)
(defclass Equivalence
(is-a Logsent)
(slot OTHER-AXIOMS
(default "((=> (Equivalence ?X)
(Exists (?P1 ?P2)
(And (Sentence ?P1) (Sentence ?P2)
(= ?X (Listof '<=> ?P1 ?P2)))))
(=>
(Exists (?P1 ?P2)
(And (Sentence ?P1) (Sentence ?P2)
(= ?X (Listof '<=> ?P1 ?P2))))
(Equivalence ?X))
(<= (Equivalence ?X)
(Exists (?P1 ?P2)
(And (Sentence ?P1) (Sentence ?P2)
(= ?X (Listof '<=> ?P1 ?P2)))))
(<=> (Equivalence ?X)
(Exists (?P1 ?P2)
(And (Sentence ?P1) (Sentence ?P2)
(= ?X (Listof '<=> ?P1 ?P2)))))
(Nth-Argument-Name Equivalence 1 '?X))")
(create-accessor read-write))
)
(defclass Quantsent
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((=> (Quantsent ?X)
(Or
(Exists (?V ?P)
(And (Indvar ?V) (Sentence ?P)
(Or (= ?X (Listof 'Forall ?V ?P))
(= ?X (Listof 'Exists ?V ?P)))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlist) (Indvar ?V))
(Or (= ?X (Listof 'Forall ?Vlist ?P))
(= ?X (Listof 'Exists ?Vlist ?P)))))))
(=>
(Or
(Exists (?V ?P)
(And (Indvar ?V) (Sentence ?P)
(Or (= ?X (Listof 'Forall ?V ?P))
(= ?X (Listof 'Exists ?V ?P)))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlist) (Indvar ?V))
(Or (= ?X (Listof 'Forall ?Vlist ?P))
(= ?X (Listof 'Exists ?Vlist ?P))))))
(Quantsent ?X))
(<= (Quantsent ?X)
(Or
(Exists (?V ?P)
(And (Indvar ?V) (Sentence ?P)
(Or (= ?X (Listof 'Forall ?V ?P))
(= ?X (Listof 'Exists ?V ?P)))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlist) (Indvar ?V))
(Or (= ?X (Listof 'Forall ?Vlist ?P))
(= ?X (Listof 'Exists ?Vlist ?P)))))))
(<=> (Quantsent ?X)
(Or
(Exists (?V ?P)
(And (Indvar ?V) (Sentence ?P)
(Or (= ?X (Listof 'Forall ?V ?P))
(= ?X (Listof 'Exists ?V ?P)))))
(Exists (?Vlist ?P)
(And (List ?Vlist) (Sentence ?P) (>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlist) (Indvar ?V))
(Or (= ?X (Listof 'Forall ?Vlist ?P))
(= ?X (Listof 'Exists ?Vlist ?P)))))))
(Nth-Argument-Name Quantsent 1 '?X))")
(create-accessor read-write))
)
(make-instance [Denotation] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (denotation $tau$)} denotes the object
denoted by the object
denoted by $tau$. A quotation denotes the quoted expression; the denotation
of any other object is $bot$.")
(OTHER-AXIOMS "((Nth-Argument-Name Denotation 1 '?X))")
)
(make-instance [Name] of Function
(Arity 2)
(Function-Arity 1)
(Documentation "The term {tt (name $tau$)} denotes the standard name for
the object denoted
by the term $tau$. The standard name for an expression $tau$ is
{tt (quote $tau$)}; the standard name for a non-expression is at the
discretion of the user. (Note that there are only a countable number of
terms in KIF, but there can be models with uncountable cardinality;
consequently, it is not always possible for every object in the universe of
discourse to have a unique name.)")
(OTHER-AXIOMS "((Nth-Argument-Name Name 1 '?X))")
)
(defclass Truth "A level-crossing relation used to state that a sentence is
true.
<H3>Notes:</H3>
<UL><B>Example: </B>(truth (quote (=> (sentence ?p) (listof (quote =>) ?p
?p))))
<BR></UL>"
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Truth 1 '?Sentence))")
(create-accessor read-write))
)
(make-instance [Defining-Axiom] of Relation
(Range Sentence)
(Domain Constant)
(Arity 2)
(Documentation "a defining axiom for a constant is a sentence that
helps define the constant. See the KIF specification
for details.")
(OTHER-AXIOMS "((Nth-Argument-Name Defining-Axiom 2 '?Sentence)
(Nth-Argument-Name Defining-Axiom 1 '?Constant))")
)
(defclass Analytic-Truth "Given a knowledge base $Delta$, the sentence {tt
(analytic-truth '$phi$)}
means that the sentence $phi$ is logically entailed by the defining axioms
of
the definitions in knowledge base $Delta$."
(is-a Sentence)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Analytic-Truth 1 '?Sentence))")
(create-accessor read-write))
)
(make-instance [Has-Cognate_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A coursework degree cannot have more than 3 credits from
Cognate courses.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Cognate_Credits 2 '?Value)
(Nth-Argument-Name Has-Cognate_Credits 1 '?Frame))")
)
;;; --- In the definition of Instance CS5804
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Class CS4000_LEVEL_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cs4000_Level_Course because Individual-Thing
;;; is already a superclass of Course.
;;;
;;; Forward declaration for external reference Course.
;;; Forward declaration for Course.
(loom:defconcept Course :only-if-no-preexisting-definition-p common-lisp:t)
(defclass Cs4000_Level_Course "CS4000 level courses"
(is-a Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cs4000_Level_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS6704
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Total_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A degree must have at least 30 quality credits for both
the Thesis and the Coursework only options.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Total_Credits 2 '?Value)
(Nth-Argument-Name Has-Total_Credits 1 '?Frame))")
)
(make-instance [Has-6000_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A degree requires a minimum of 3 credits from 6000
level.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-6000_Credits 2 '?Value)
(Nth-Argument-Name Has-6000_Credits 1 '?Frame))")
)
;;; --- In the definition of Class CS5000_LEVEL_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cs5000_Level_Course because Individual-Thing
;;; is already a superclass of Course.
;;;
(defclass Cs5000_Level_Course "CS5000 Level Courses"
(is-a Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cs5000_Level_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS5204
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5114
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS4004
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5714
;;;
;;; Unknown construct in CLIPS.
;;;
;;; Forward declaration for external reference Degree.
;;; Forward declaration for Degree.
(loom:defconcept Degree :only-if-no-preexisting-definition-p common-lisp:t)
(defclass Coursework
(is-a Individual-Thing Degree)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Coursework 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Class COGNATE_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cognate_Course because Individual-Thing
;;; is already a superclass of Course.
;;;
(defclass Cognate_Course "Coursework students must take one cognate course
which is a non CS course."
(is-a Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cognate_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS6724
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance ISE5134
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Grade] of Relation
(Range Number)
(Domain Course)
(Arity 2)
(Documentation "a student receives a grade upon completing a course")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Grade 2 '?Value)
(Nth-Argument-Name Has-Grade 1 '?Frame))")
)
;;; --- In the definition of Instance CS6604
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-5000_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A degree requires a multitude of credits from 5000 level
or higher, the majority of which will be 5000 level.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-5000_Credits 2 '?Value)
(Nth-Argument-Name Has-5000_Credits 1 '?Frame))")
)
;;; --- In the definition of Class CS5994_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cs5994_Course because Individual-Thing
;;; is already a superclass of Cs5000_Level_Course.
;;;
(defclass Cs5994_Course "A Thesis must have between 6 and 9 credits from
CS5994 (research) courses. CS5994 courses do not count towards the
coursework option."
(is-a Cs5000_Level_Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cs5994_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS4984
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-5994_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A Thesis degree cannot have more than 9 credits from
CS5994.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-5994_Credits 2 '?Value)
(Nth-Argument-Name Has-5994_Credits 1 '?Frame))")
)
;;; --- In the definition of Instance CS5314
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5704
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5974
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-5974_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A coursework degree cannot have more than 6 credits from
CS5974 level.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-5974_Credits 2 '?Value)
(Nth-Argument-Name Has-5974_Credits 1 '?Frame))")
)
(make-instance [Has-Credits] of Relation
(Range Number)
(Domain Course)
(Arity 2)
(Documentation "Each completed requirement satisfying course is worth 3
credits")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Credits 2 '?Value)
(Nth-Argument-Name Has-Credits 1 '?Frame))")
)
(defclass Course
(is-a Individual-Thing Degree)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Course 1 '?X))")
(create-accessor read-write))
(multislot Has-Course_Number
(create-accessor read-write)
(type Number))
(multislot Has-Prerequisite
(create-accessor read-write)
(type INSTANCE))
(multislot Has-Course_Availability
(create-accessor read-write)
(type Number))
(multislot Has-Course_Name
(create-accessor read-write)
(type String))
(multislot Has-Department
(create-accessor read-write)
(type String))
(multislot Has-Credits
(create-accessor read-write)
(type Number))
(multislot Has-Grade
(create-accessor read-write)
(type Number))
)
(make-instance [Has-Department] of Relation
(Range String)
(Domain Course)
(Arity 2)
(Documentation "Each course has a department. We are only concerned
with courses within the CS department")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Department 2 '?Value)
(Nth-Argument-Name Has-Department 1 '?Frame))")
)
;;; --- In the definition of Instance CS5104
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5984
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5516
;;;
;;; Unknown construct in CLIPS.
;;;
(defclass Thesis
(is-a Degree Individual-Thing)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Thesis 1 '?X))")
(create-accessor read-write))
)
(make-instance [Exists_Degree] of Named-Axiom
(Documentation "Degree exists if total credits are >= 30 for either
thesis or coursework") (OTHER-AXIOMS "((=>
(Degree)
(Or
(And
(Thesis
?Has-Total_Credits)
(>=
?Has-Total_Credits
30))
(And
(Coursework
?Has-Total_Credits)
(>=
?Has-Total_Credits
30)))))")
)
;;; --- In the definition of Instance CS5485
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Class CS5974_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cs5974_Course because Individual-Thing
;;; is already a superclass of Cs5000_Level_Course.
;;;
(defclass Cs5974_Course "CS5974 is an Independent Study Course. A student
may not use more than 6 CS5974 Credits for a coursework degree. CS5974 does
not count towards a thesis degree"
(is-a Cs5000_Level_Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cs5974_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS5604
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Class CS6000_LEVEL_COURSE
;;;
;;; Individual-Thing has not been included in the superset list
;;; of Cs6000_Level_Course because Individual-Thing
;;; is already a superclass of Course.
;;;
(defclass Cs6000_Level_Course "CS6000 Level Courses"
(is-a Course)
(slot OTHER-AXIOMS
(default "((Nth-Argument-Name Cs6000_Level_Course 1 '?X))")
(create-accessor read-write))
)
;;; --- In the definition of Instance CS5614
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Course] of Relation
(Range Course)
(Domain Degree)
(Arity 2)
(OTHER-AXIOMS "((Nth-Argument-Name Has-Course 2 '?Y)
(Nth-Argument-Name Has-Course 1 '?X))")
)
;;; --- In the definition of Instance CS6204
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Exists_Thesis] of Named-Axiom
(Documentation "A Thesis exists when certain minimum requirements are
met.") (OTHER-AXIOMS "((=>
(Thesis)
(And
(>=
Has-Total_Credits
30)
(=<
Has-5994_Credits
9)
(>=
Has-5994_Credits
6)
(=<
Has-4000_Credits
3)
(>=
Has-6000_Credits
3)
(>=
Breadth
4))))")
)
;;; --- In the definition of Instance CS5515
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5214
;;;
;;; Unknown construct in CLIPS.
;;;
;;; --- In the definition of Instance CS5014
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Course_Name] of Relation
(Range String)
(Domain Course)
(Arity 2)
(Documentation "Each course has a class name")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Course_Name 2 '?Value)
(Nth-Argument-Name Has-Course_Name 1 '?Frame))")
)
;;; --- In the definition of Instance CS5994
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Exists_Coursework] of Named-Axiom
(Documentation "A Coursework exists when certain minimum requirements are
met.") (OTHER-AXIOMS "((=>
(Coursework)
(And
(>=
Has-Total_Credits
30)
(=
Has-Cognate_Credits
3)
(=<
Has-4000_Credits
3)
(=
Has-5974_Credits
3)
(>=
Has-6000_Credits
3)
(>=
Breadth
5))))")
)
(make-instance [Has-Course_Availability] of Relation
(Range Number)
(Domain Course)
(Arity 2)
(Documentation "a course is available or not")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Course_Availability 2 '?Value)
(Nth-Argument-Name Has-Course_Availability 1 '?Frame))")
)
;;; --- In the definition of Instance CS5034
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Prerequisite] of Relation
(Range Course)
(Domain Course)
(Arity 2)
(Documentation "Some courses has prerequisite courses")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Prerequisite 2 '?Value)
(Nth-Argument-Name Has-Prerequisite 1 '?Frame))")
)
;;; --- In the definition of Instance CS4014
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-Course_Number] of Relation
(Range Number)
(Domain Course)
(Arity 2)
(Documentation "Each Course has a course number containing four digits")
(OTHER-AXIOMS "((Nth-Argument-Name Has-Course_Number 2 '?Value)
(Nth-Argument-Name Has-Course_Number 1 '?Frame))")
)
(make-instance [Breadth] of Function
(Range Number)
(Domain Degree)
(Arity 2)
(Function-Arity 1)
(Documentation "Courses must be taken in a variety of computer-science
related areas. Courses must be taken with several different second digits
in accordance with the restriction placed on the subclass (thesis or
coursework).")
(OTHER-AXIOMS "((Nth-Argument-Name Breadth 1 '?Frame))")
)
;;; --- In the definition of Instance CS6804
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Has-4000_Credits] of Relation
(Range Number)
(Domain Degree)
(Arity 2)
(Documentation "A degree cannot have more than 6 credits from 4000
level.")
(OTHER-AXIOMS "((Nth-Argument-Name Has-4000_Credits 2 '?Value)
(Nth-Argument-Name Has-4000_Credits 1 '?Frame))")
)
(defclass Degree
(is-a Thing)
(slot OTHER-AXIOMS
(default "((=>
(Or
(And (Thesis ?Has-Total_Credits) (>= ?Has-Total_Credits
30))
(And (Coursework ?Has-Total_Credits)
(>= ?Has-Total_Credits 30)))
(Degree))
(Nth-Argument-Name Degree 1 '?X))")
(create-accessor read-write))
(multislot Has-4000_Credits
(create-accessor read-write)
(type Number))
(single-slot Breadth
(create-accessor read-write)
(type Number))
(multislot Has-Course
(create-accessor read-write)
(type INSTANCE))
(multislot Has-5974_Credits
(create-accessor read-write)
(type Number))
(multislot Has-5994_Credits
(create-accessor read-write)
(type Number))
(multislot Has-5000_Credits
(create-accessor read-write)
(type Number))
(multislot Has-6000_Credits
(create-accessor read-write)
(type Number))
(multislot Has-Total_Credits
(create-accessor read-write)
(type Number))
(multislot Has-Cognate_Credits
(create-accessor read-write)
(type Number))
)
;;; --- In the definition of Instance CS5304
;;;
;;; Unknown construct in CLIPS.
;;;
(make-instance [Credits] of Named-Axiom
(Documentation "Three credits are received for every course that
satisfies a requirement.") (OTHER-AXIOMS "((=>
(=
Has-Credits
3)
(And
(Not
(Has-Course_Number
5904))
(Not
(Has-Course_Number
5944))
(Not
(Has-Course_Number
5974))
(Not
(Has-Course_Number
7994))
(Or
(And
(Has-Department
"CS")
(=>
(Has-Course_Number
5994)
(<
Has-5994_Credits
9))
(=>
(And
(>
Has-Course_Number
4000)
(<
Has-Course_Number
5000))
(<
Has-4000_Credits
3))
(=>
(Has-Total_Credits
21)
(>=
Breadth
2))
(=>
(Has-Total_Credits
24)
(>=
Breadth
3))
(=>
(Has-Total_Credits
27)
(>=
Breadth
4)))
(And
(Has-Department
"CS")
(=>
(Has-Course_Number
5974)
(<
Has-5974_Credits
3))
(=>
(And
(>
Has-Course_Number
4000)
(<
Has-Course_Number
5000))
(<
Has-4000_Credits
3))
(=>
(Has-Total_Credits
18)
(>=
Breadth
2))
(=>
(Has-Total_Credits
21)
(>=
Breadth
3))
(=>
(Has-Total_Credits
24)
(>=
Breadth
4))
(=>
(Has-Total_Credits
27)
(>=
Breadth
5))
(=>
(Has-Department
"Cognate")
(<
Has-Cognate_Credits
3)))))))")
)
