Daneel Pang's Ontolingua paper
Tom Gruber <Gruber@sumex-aim.stanford.edu>
Full-Name: Tom Gruber
Message-id: <2870816529-5881409@KSL-Mac-69>
Date: Fri, 21 Dec 90 17:02:09 PST
From: Tom Gruber <Gruber@sumex-aim.stanford.edu>
To: ontolingua@sumex-aim.stanford.edu
Subject: Daneel Pang's Ontolingua paper
Enclosed is a paper by Daneel Pang, who was a MS student who
implemented a first version of ontolingua for Epikit, LOOM, and KIF.
In addition to making the routine stuff like define-class work, he
explored some extensions motivated by the needs of our port of DME off
of Cyc.
I am sending this to describe the first-cut syntax that he implemented
and to introduce some of issues involved in extending the language to
support productions and possible worlds. I don't view the latter
capability as designed, much less implemented, but Pang did a good bit
of thinking on what might be done.
The laper is in LaTeX format, but requires a doublespace.sty file. If
you don't have this file, let me know and I'll send it to you. Be
warned that the paper is long, because of spacious formatting.
--tom
% -*- Mode:TeX -*-
\documentstyle[11pt, doublespace]{report}
\begin{document}
\title{{\Huge OntoLingua} \\[4mm]
{\em The Syntax, Semantics, and Implementation}}
\author{Pang, Swee-Chee}
\maketitle
\setlength{\textheight}{8in}
\setlength{\textwidth}{6.5in}
\setlength{\oddsidemargin}{0.8in}
\setlength{\evensidemargin}{0.8in}
\setlength{\topmargin}{0.5in}
\renewcommand{\baselinestretch}{1.24}
%% Basic Macros for LaTeX commands.
{\obeyspaces\global\let =\ }
\def\uncatcodes{\def\do##1{\catcode`##1=12}\dospecials}
\def\setupverb{\tt\spaceskip=0pt% % Make sure we get fixed tt spacing
\parskip=0pt plus .05\baselineskip\parindent=0pt%
\uncatcodes\catcode`\\=0\catcode`\{=1\catcode`\}=2\catcode`\$=3%
\obeylines\obeyspaces%
}
{\catcode`\^^M=13\gdef\verbatimgobble#1^^M{}}
\def\xverb{\begingroup\setupverb}
\let\xendverb=\endgroup
\def\asis{\xverb\helpcode}
\def\helpcode#1{#1\xendverb}
\newcommand{\asisblock}[0]{\begin{singlespace}\begin{quote}\xverb\helpasisblock}
\newcommand{\helpasisblock}[1]{\verbatimgobble #1\xendverb\end{quote}\end{singlespace}}
\newcommand{\allonto}{{\rm Ontolingua\ }}
\newcommand{\allontons}{{\rm Ontolingua}}
\newcommand{\ttonto}{{\tt ontolingua\ }}
\newcommand{\ttontons}{{\tt ontolingua}}
\newcommand{\onto}{{\bf OntoLingua\ }}
\newcommand{\ontons}{{\bf OntoLingua}}
\newcommand{\st}{\;\ni\;}
\newcommand{\var}{\nu}
\newcommand{\proves}{\vdash}
\newcommand{\entails}{\models}
\newcommand{\nec}{\Box}
\newcommand{\poss}{\Diamond}
\newcommand{\implies}{\Rightarrow}
\newcommand{\suffice}{\Leftarrow}
\newcommand{\equival}{\Leftrightarrow}
\newcommand{\valof}{{\sl s}_{\sl iv}}
\newcommand{\truthof}{{\sl t}_{\sl iv}}
\newcommand{\andl}{\wedge}
\newcommand{\orl}{\vee}
\newcommand{\sline}{\noindent\\ \rule[5pt]{5.4in}{1pt}\\}
%%%%%%%%%%%%%%%%%%%%%%%%%%
\tableofcontents
%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Introduction}
The word \allonto is {\em most} likely the condensation of the words:
Ontology and InterLingua. The intention of having \onto
is to provide a standardized {\em syntax} for ontologies which attempts to
encompass the {\em semantics} and intentions of several major philosophy of
knowledge representations.
It is hoped that we will be able to then translate a knowledge base/ontology
described in \onto into a system which is an implementation
of any of those philosophy with reasonable efficiency and consistency,
and such that the resulting translation is the way someone with some
proficiency in the target system would have written it.
To that end, we have a first attempt {\em implementation}, called
simply \ttontons, which conforms to the syntax which we have
developed and which would be specified in detail in the following chapter.
This system has been implemented to translate to {\bf Kif},
{\bf Epikit} and {\bf Loom}.
Currently there are attempts to translate this into {\bf CycL}
and {\bf Algernon} as well.
Since the \allonto is still in the process of being defined, changes would be
bound to occur and it would occur frequently.
The idea of a documentation for the \allontons, therefore, is only to
capture enough of the system to allow people who wish to find out what
it is about to have a starting point.
But what is more important, it is hoped that one may capture the
original thoughts and intentions that had become what is the
\allontons.
What follows will be a list of all the commands, and syntax and
semantics of the \ttonto implementation, with some
explanations as to the \onto {\sl whys} and {\sl what-fors}
where it has been recognized and deemed appropriate to include.
For the rest of this document, as was consistent in this chapter, the
word \onto would be intended to mean the idea and concept,
the word \ttonto that of the implementation and
the word \allonto as an abbreviation for ``both the \ttonto and \ontons.''
\chapter{Basic \ttonto form}
\section{Formulating \ttonto}
In designing the forms for the \ttontons, the current assumption
for an underlying knowledge system must be one of a {\em frame based}
approach (FBA), or a {\em logic based} approach (LBA) with a
sufficiently powerful inference engine to handle multiple complex knowledge
bases.
With this in mind and other related issues, the implementation has also
attempted to adhere to the following ideas:
\vspace{-6mm}
\begin{singlespace}
\begin{itemize}
\item {\bf readable}\\[1mm]
The user should be able to easily recognize, via a glance of the
knowledge as depicted in it's \ttonto form, the essential
details and the knowledge that is being captured.
\item {\bf recognizable}\\[1mm]
The translated result should be in some correspondence with the
original ontolingua form that it would be
easy for a user versed in the target system to locate the translated
forms from the original \ttonto form.
\item {\bf translatable}\\[1mm]
Each form and keyword be directly translatable in a satisfactory fashion into
the underlying knowledge system.
\item {\bf unambiguous}\\[1mm]
Each form should stand clearly for some distinct notion and each
expression, symbol be unambiguously mapped into it's proper syntax.
\item {\bf unbiased}\\[1mm]
As recognition that both the FBA and LBA have
merits, limitations, restrictions and a large community of supporting
arguments, as well as the fact that there might exists some
correspondence of one form with another, \ttonto will adopt a
form which attempts to capture the essential syntax needed for each
form.
\end{itemize}
\end{singlespace}
\vspace{-2mm}
Although these ideas do not have definitive or precise restrictions, nor do
they seem to have clear boundaries, they
nonetheless are reasonable and important considerations which had
shaped the resulting format as would be presented.
\section{Basic logical sentences}
The notion of a sentence here is that which constitute a legal {\em logic}
sentence in \ttonto as well as \ontons.
The logical sentences as constructed in accordance to {\bf
KIF} are legal sentences.\footnote{This is in accordance to
the fact that, \onto, as it stands, does not intend to
become {\em yet another standard}, but wishes to build alongside and
on top of some existing standard}
However, some extensions were found necessary because {\bf KIF},
in it's current form, is not as yet complete.
The \onto introduces the keywords {\bf the}, {\bf bagof},
and {\bf setof}. We may introduce also, the keyword {\bf true\_in} in a
latter implementation.
\subsection{Bagof and Setof}
The keywords {\bf bagof} and {\bf setof} were found to be convenient
components in describing a knowledge which utilize some form of
{\em Axioms}, (for example, {\em Newton's Law} or {\em Kirchoff's Law}) where
one finds the need to state things in respect of all or some of the
elements of a set satisfying some arbitrary criteria.
The syntax for {\bf setof} and {\bf bagof} are similar.
Where $\psi$ is a logical sentence, $\var$ is a variable, we have:
\asis{([setof/bagof] $\var$ $\psi$)} is a valid logical sentence,
and
\begin{eqnarray*}
\lefteqn{\valof((\mbox{\bf setof}\;\var\;\psi)) =
\valof((\mbox{\bf list}\;\tau_1 \cdots \tau_n))}\\
&\st (&
(i \neq j \implies \tau_i \neq \tau_j) \andl \\
&&(\forall \tau)(\truthof(\var|\tau)(\psi) = \mbox{{\sl true} iff}\;
(\exists i) \valof(\tau) = \valof(\tau_i))
\end{eqnarray*}
Note here that the use of ``{\bf list}'' is unsatisfactory but is the only form
provided by {\bf KIF} adequate for the purpose.
The line ``$\tau_i \neq \tau_j$'' should also be noted as being different
>From that of ``$\valof(\tau_i) \neq \valof(\tau_j)$'' with the former being
{\em not logically equivalent} and not opened to interpretation as is the
latter.
The {\bf bagof} keyword may be similarly defined, where it differs from the
{\bf setof} operator in that for each proof, there is a unique $\tau_i$, thus
the elements in a {\bf bagof} may be duplicated, if there is more than one
proof for it.
Those familiar with {\bf PROLOG} will recognize these as being similar to
their peers.\footnote{Note however that where no proof exists, PROLOG reports
failure whereas this produces the list ``({\bf list})'' corresponding to the
notion of an empty list.}
\subsection{The}
The keyword {\bf the} was necessary because of the difference in
the treatment of relations/predicates and functions between FBA and LBA.
Here, we first introduce that difference and it's consequences or
justifications, then we introduce the \onto at reconciliation by
introducing the {\bf the} keyword.
In attempting to establish a correspondence/mapping between LBA and FBA,
in terms of concepts, relations, predicates, functions, an acceptable
mapping, and the one adopted by \onto is thus:
\begin{itemize}
\item FBA's operators into LBA's operators [eg not, and, or]
\item FBA's concept into LBA's unary predicate and vice versa.
\item FBA's relation into LBA's predicate and vice versa.
\item FBA's function into LBA's function and vice versa.
\end{itemize}
There is, obviously, a commitment here that there are {\em no} unary relation
which can not be treated as some form of concept.
This commitment, we think, is a reasonable one.
However, there is yet another problem.
In LBA, there is a commitment to a strict differentiation between function and
predicates in that one is strictly a ``term yielding'' object while the other
is a ``truth yielding'' object.\footnote{here I use the words object, term
yielding and truth yielding loosely, appealing to the reader to understand the
mapping invoked. Otherwise, the reader is encouraged to seek out the mail file
which discusses this issue in more detail.} In FBA, the distinction between
these are not as strict.
Thus, if ``{\tt father-of}'' is a function and ``{\tt father}'' a
predicate, the sentences
{\tt (= (father-of cain) adam)}'' and
``{\tt (father adam cain)}''
are valid sentences in both FBA and LBA, but the sentence
``{\tt (= (father adam) cain)}'' is a valid FBA sentence but not a
valid LBA sentence, similarly the sentence
``{\tt (father-of cain adam)}''.
If we adopt {\bf KIF}'s approach, which is one of LBA, we run into the
following compromises:
\begin{itemize}
\item
in the FBA standpoint, functions are a special case of relations, being
single-valued, and this is a valid standpoint, from the point of functions and
relations as defined in Mathematics. In choosing to adopt LBA, we would thus
have a {\bf bias}, countering one of the ideas we had decided to adhere to.
\item
in FBA terminology, the use of ``role chains'' is a common practice, and the
denotation of role chains might imply some form of optimization as well
(polynomial time search, perhaps). In choosing to adopt LBA, we would thus
loose the capability of encoding the intentional usage of such forms, and to
thus fail the criteria of both {\bf translatable} and {\bf recognizable}.
\end{itemize}
If we, however, adopt the FBA standpoint, the translation into LBA would be
problematic, if possible at all without assumptions of ``states'' or ``define
before use'' or some such.
The problem arises since the ``function'' appearing in a ``term yielding''
position might actually be used as a ``predicate'' earlier or later, and vice
versa.
This violates
\begin{itemize}
\item {\bf readable}\\[1mm]
since the entire content has to be read, analyzed
before the decision can be made,
\item {\bf recognizable}\\[1mm]
since the correspondence between LBA and \ttonto is now
one which violates some basic assumptions of LBA.
\item {\bf unambiguous}\\
upto, and unless we adopt a ``first use'' policy or some
such, the translation could be incompatible depending on the order of
interpretation and file loading.
\end{itemize}
Having thus found ourselves trapped, it was decided that we adopt a keyword, a
user conscious escape hatch which would allow both LBA and FBA to function
without there being any argument and maintaining an easy correspondence.
Thus, with the above in mind, and giving minimal change to both form, we adopt
the following syntax for the keyword {\bf the}:
where ``$(\psi\; \tau_1 \cdots \tau_n\; \tau)$'' is a valid \ttonto
relation, the form ``$(\psi\; \tau_1 \cdots \tau_n)$'' is a
valid function which will be used to denote each ``$\tau$'' which satisfied
the relation, {\em ie}, dropping all but the last term of a relation yields a
function denoting that last term.
More precisely,
\begin{eqnarray*}
\lefteqn{\truthof((\psi\; \var_1 \cdots \var_i\;
(\mbox{\bf the}\;(\phi\;\tau_1 \cdots \tau_n))\;
\var_j \cdots \var_m))}&&\\
&=&\truthof((\mbox{\bf and}\;(\phi\;\tau_1 \cdots \tau_n\; \tau)\;
(\psi\; \var_1 \cdots \var_i\; \tau\; \var_j \cdots \var_m)))
\end{eqnarray*}
where {\bf and} is as defined in {\bf KIF}, except it should be emphasized that
in order to capture the intention of ``role chains'' the order of execution
should be maintained as inside-out, left-to-right for this translation, else
the translation should be reversed.
It should be noted also that this is the translation performed into an LBA
and the keyword {\bf the} will be simply removed for an FBA.
Lastly, the {\bf the} keyword may be nested and it is possible for
multiple {\bf the} forms to occur in one sentence.
\section{The whole sentence}
Any {\bf KIF} sentence would form a valid \ttonto sentence, but not vice
versa.
Although it is intended that the extensions be suggested to the {\bf KIF}
group for inclusion in the next KIF release if so desired.
Thus, in refinement:
\begin{itemize}
\item A valid {\bf KIF} logical sentence is a valid \ttonto logical sentence.
\item
The \onto extensions are valid \ttonto logical sentences if written in their
stated valid syntactic form.
\item
Any valid \ttonto logical sentences combined using one of the valid {\bf KIF}
sentence combination rules forms a valid \ttonto logical sentence.
(examples, ``({\bf and} $\phi$ $\psi$)'' and ``({\bf exists} $\var$ $\phi$)''
are valid \ttonto logical sentences if $\phi$ and $\psi$ are valid \ttonto
sentences while $\var$ is a valid \ttonto variable, which is a valid {\bf KIF}
variable).
\item No other sentences are valid \ttonto sentences.
\end{itemize}
\chapter{Basic Set of Commands}
\section{Full forms}
Having spent the previous chapter describing the constituent of a valid
\ttonto logical sentence, it is time to go further and describe what
constitute an \ttonto statement, or command.
This is what is normally alluded to when one comments on ``the ontolingua
form.''
Following this will be sections which will describe each of the forms that
were developed for this first \ttonto implementation.
As a policy, each and every \ttonto form comes in a dual LISP macro and
function pair.
The reason for this is simply that the macro form enables the user to, wherein
it is possible to so determined in compile time all the necessary formats,
macro-expand and compile the ontolingua forms and to later be able to deal
with that compiled form without the need of having the \ttonto package
present.
This is in accordance and proof that \ttontons, as it stands, is
stateless (the translations are deterministic and complete, without need or
requirements for the \ttonto to rely on order and sequence of compilation),
and that the \ttonto is merely a translation system and not one which
provides its own inference mechanism or any such that is required for the
{\em runtime} support of the system.
The command words, to date, are (macro versions):
define-relation, define-class, define-function, define-production,
define-world, define-instance, define-assertions,
perform-in-world, perform-local-world,
tellm,
query-find-one, query-find-all, query-provable, query-find-world, query-info,
and
reset-knowledge-base.
The functional versions of these are formed by substituting
``create-'' for ``define-'',
``do-'' for ``perform-'',
``tellf'' for ``tellm'',
``do-'' for ``query-'',
and ``reset-'' is replaced by ``renew-''.
Admittedly, some of these words thus formed need to be improved,
but they are currently the simplest subset to which one may include duality
easily. More maybe added and deleted later, or, most likely, modified,
so do read the online documentation for the \ttonto often, since these are
always and should continue to be diligently updated.
\pagebreak
\section{The Commands}
Following this, all but the {\em world} keywords will be explained in their
own subsection.
The concept and possible development of worlds will be introduced in the next
chapter.
\pagebreak
\subsection{define-relation}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-RELATION (MACRO):
RELATION-NAME
VAR-LIST
DOCUMENTATION
&KEY
(DEFINITION NIL)
(PRIMITIVE-DEFINITION NIL)
(EQUIVALENT NIL)
(SUFFICIENT NIL)
(IMPLIES NIL)
(DEFAULT-IMPLIES NIL)
(SECOND-ORDER NIL)
}
\vspace{-0.5in}\sline
This command defines a relation ($n$-ary, $n > 1$)
named {\tt RELATION-NAME}.
It is followed by a list of variables which would be used to denote the arity
as well as serving as the formal parameters for the relation in this form.
As with most every \ttonto form, a documentation string is requested with
the form, this documentation may be retrieved by a query for the
documentation on the relation name.
The keywords ``{\bf Definition}'' and ``{\bf Primitive-definition}'' are
mutually exclusive keywords in this form and correspond to the equivalent
non-primitive and primitive definitions available in both the {\bf KL-ONE}
community as well as in the {\bf KIF} document.
Using logic notation, a definition is a necessary and sufficient condition
whilst a primitive definition is but a necessary one, although this
explanation does not seem to capture the entirety of it, it is nonetheless
the acceptable logically translation thus far. Exactly {\bf ONE} of these 2
keywords must be present. The argument to each of these is a valid \ttonto
sentence.
The following {\bf Equivalent}, {\bf Sufficient} and {\bf Implies} keywords
correspond to places where one may put down sentences to which this relation
maybe equivalently (necessary and sufficient, or ``$\equival$''),
sufficiently ($\suffice$), or necessarily ($\implies$) related to.
The argument acceptable to each of these is a valid \ttonto logic sentence.
{\bf Default-implies} indicates the default implication rule involving the
current relation. What follows should be a simple list of \ttonto relation or class sentence (ie, where $\psi$ is a relation, or class, ($\psi$ @l) is a valid relation or class sentence).
At times, one may wish to make {\bf Second-order} statements regarding a
relation, like that it is {\bf asymmetric} or a {\bf subrelation} of some
relation. These are second order statements in as much as the relation $\psi$
appears as an ``instance'' in the statement $(\mbox{\bf asymmetric}\; \psi)$.
For a list of currently available second-order keywords, see
the section on Second Order Keywords.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(define-relation father-of (father child)
``Father is the father-of Child''
:primitive-definition (and (human-male father)
(human child))
:implies (child-of child father)
:default-implies (married father)
)
}
Which defines the relation ``father-of'' stating that (primitive-definition)
the father must be a human-male and the child, a human.
Also the ``implies'' sentence states that
``if f is a father-of c, then c is a child-of f'', since the ``if'' part of
the ``implies'' is omitted (implicit) in this structure.
The default-implies line states that unless the father is otherwise known not
to be married, the father should be considered married.
\asisblock{
(define-relation father-of (father child)
``Father is the father-of Child''
:definition (and (parent-of father child)
(human-male father)))
:second-order ((irreflexive father-of)
(asymmetric father-of))
)
}
This similarly defines a ``father-of'' relation which states that
(definition) a ``father-of'' relation is simply a ``parent-of'' relation
where the ``father'' is a ``human-male'' (and nothing more?),
and that the relation is Irreflexive and Asymmetric.
\pagebreak
\subsection{define-class}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-CLASS (MACRO):
CLASS-NAME
VAR-LIST
DOCUMENTATION
&KEY
(DEFINITION NIL)
(PRIMITIVE-DEFINITION NIL)
(EQUIVALENT NIL)
(SUFFICIENT NIL)
(IMPLIES NIL)
(SECOND-ORDER NIL)
(DEFAULT-IMPLIES NIL)
}
\vspace{-0.5in}\sline
This command defines a class (concept or unary-predicate) which is named
{\tt CLASS-NAME}.
It is followed by a list of variables (should have exactly 1 element in the
list) just as with {\tt DEFINE-RELATION}.
In fact, other than the fact that it is called a class and is unary, there is
no syntactic difference between this and {\tt DEFINE-RELATION}.
See {\tt DEFINE-RELATION} for more information.
Noted here is that there are some second order keywords applicable only to a
class and some only to relations, and these will be stated as such where they
are defined.
\pagebreak
\subsection{define-function}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-FUNCTION (MACRO):
FUNCTION-NAME
ARG-LIST
DOCUMENTATION
&KEY
(LISP-BODY NIL)
(KIF-FUNCTION NIL)
}
\vspace{-0.5in}\sline
Defines a function named {\tt FUNCTION-NAME} with the given {\tt ARG-LIST} as
the argument list.
This defines the arity and formal parameters of the function.
Exactly one of the {\tt LISP-BODY} or {\tt KIF-FUNCTION} option must be
provided in this form.
This definition of function follows the {\bf KIF} intentions.
{\tt LISP-BODY} must be a valid lisp body, and {\tt KIF-FUNCTION} a
valid term-yielding KIF term.
The provision of the normal {\tt KIF-FUNCTION} definition allows incomplete
function specifications in {\bf KIF} or defining it in full using pure
{\bf KIF}.
The {\tt LISP-BODY} form allows the knowledge base to fall back on the LISP
code to perform the necessary task, and should not be viewed as an
endorsement to the utilization of ``magic'' functions.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(define-function intpower (x y)
``Function which returns X to the power of Y.
Where Y is assumed Integer.''
:lisp-body (if (<= y 0)
1
(* x (intpower x (1- y))))
)
}
Which defines a LISP function ``intpower'' which can be utilized by the
knowledge base as an integral part of it's own function definition.
\asisblock{
(define-function grandparent (child)
``Returns the grandparent of Child.''
:kif-function (parent (parent child))
)
}
Which states simply that the grandparent of a child may be found by
looking at the parent of the parent of child.
\pagebreak
\subsection{define-production}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-PRODUCTION (MACRO):
PRODUCTION-NAME
DOCUMENTATION
CONDITION
&BODY
ACTIONS
}
\vspace{-0.5in}\sline
Defines a ``production'' rule which essentially is the place where one
is provided with an escape hatch away from the base inference engine
into the user's own set of LISP, or \ttonto actions.
The condition matched would allow the actions to be executed, which is
essentially a LISP method call.
The condition part must be a valid \ttonto sentence, and
the action part, any list of valid \ttonto statement or LISP statements.
The name of ``production'' is perhaps a misnomer, there is no sense of
conflict resolution and such, the system is merely one of ``fire when
activated'' by the knowledge base, and there is no way of predicting which
order or that one or many of these satisfying similar conditions would be
fired. So, in a sense, utilizing productions to create a production system
would be a horrible mistake. And that was not the intention. The intention
is to provide a command allowing the user to place an easy hook into the
inference engine to perhaps activate yet another set of routines.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(define-production new-rabbits
``Creates new instances of rabbits''
(and (pregnant \$x) (rabbit \$x))
(format t ``~%~A is pregnant and giving birth to:~%'' \$x)
(let ((newrabbit (form-name-from \$x)))
(create-instance newrabbit
``Yet another rabbit.''
:class '(rabbit)
:assertions (child-of \$x)))
)
}
Which speaks for itself. Note that the condition is 1 sentence whereas the
action part consists of as many sentences as is required, and note the mix of
LISP commands with \ttonto statements.
\pagebreak
\subsection{define-instance}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-INSTANCE (MACRO):
INSTANCE-NAME
DOCUMENTATION
&KEY
(CLASSES '(THING))
(ASSERTIONS NIL)
}
\vspace{-0.5in}\sline
Defines a named instance {\tt INSTANCE-NAME} which is an instance of the
classes {\tt CLASSES} (thus, an instance can be an instance of several
classes, without preference).
Classes should be a list of classes (defaults to the generic \ttonto defined
``THING'' class, see {\tt RESET-KNOWLEDGE-BASE}).
The {\tt ASSERTIONS} is a list of assertions of which the first argument is
implicitly the instance, see example below.
This is, in a fashion, the same policy of the ``slot-value'' pairs in a FBA
wherein the first argument to the relation is implicit in the ``frame'' of
the instance.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(define-instance kathy
``The frame denoting Kathy.''
:classes (person female)
:assertions ((child-of beth) (occupation nurse))
)
}
Which states that Kathy is an instance of a person and a female (ie, a female
person), and that she is both the child of Beth and a nurse, where the
sentence ``(child-of beth)'' is assumed to intend the sentence ``(child-of
kathy beth)'' (implicit first argument).
\pagebreak
\subsection{define-assertion and tellm}
\sline\vspace{-0.5in}
\asisblock{
DEFINE-ASSERTIONS (MACRO):
TITLE
DOCUMENTATION
&BODY
ASSERTIONS
}\vspace{-0.5in}\sline\vspace{-0.5in}\asisblock{
TELLM (MACRO):
&REST
ASSERTIONS
}
\sline
The {\tt ASSERTIONS} for both forms are any list of valid \ttonto logic
sentences.
Thus, both are methods by which one may key in an arbitrary large amount of
\ttonto logic sentences.
However, in ``define-assertion,'' there is a {\tt TITLE} and
{\tt DOCUMENTATION} to fill in.
The intention, therefore, is that under the ``define-assertion'' form, one
groups assertions which are meaningful in some ways, like ``Newton's Laws''
or some such.
Also, use of too many ``tellm''s is discouraged since it implies a
disorganization of the knowledge base might be occurring, and the benefits
and clarity of the knowledge base via the other forms would be lost.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(define-assertions NewtonsLaws
``The 3 Laws of Newtonian Physics''
...
)
}
\asisblock{
(tellm (==> (unique \$ro \$x)
(true (list '=> (list \$ro \$x '\$y)
(list \$ro \$x '\$z)
(list '= '\$y '\$z)
)
)
)
)
}
\pagebreak
\subsection{query-find-[one/all] and query-provable}
\sline\vspace{-0.5in}
\asisblock{
QUERY-FIND-[ONE/ALL] (MACRO):
VAR-LIST
EXPR
}\vspace{-0.5in}\sline\vspace{-0.5in}\asisblock{
QUERY-PROVABLE (MACRO):
EXPR
}
\vspace{-0.5in}\sline
The 3 basic query forms which are necessary for a system.
{\tt Query-find-one} returns upon the first successful ``prove'' of {\tt
EXPR} and binds the variables in {\tt VAR-LIST} with the successful binding
on {\tt EXPR}, whereas {\tt query-find-all} returns a list of the bindings
for the exhaustive search for bindings into {\tt EXPR} which are satisfied.
Both forms return {\em nil} where they fill.
{\tt Query-provable} returns {\em nil} where it fails (not provable or
contradiction) or non-nil where it succeeds.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(query-find-one (\$x \$y) (mother-of \$x \$y))
}
will return {\em (Anne John)} if it is indeed true in the knowledge base
that Anne is the mother of John.
If the {\tt all} form was used instead, the system would return
{\em ((Anne John) (Jane Kathy) ...)}, giving the exhaustive list.
Thus,
\asisblock{
(provable (mother-of Anne \$x))
}
will be non-nil, but
\asisblock{
(provable (mother-of John Anne))
}
will return {\em nil}.
\pagebreak
\subsection{query-info}
\sline\vspace{-0.5in}
\asisblock{
QUERY-INFO (MACRO):
SYMBOL
&OPTIONAL
(INFO-TYPE :TYPE)
}
\vspace{-0.5in}\sline
In recognition that it is sometimes desired to know what type a symbol is, or
to get back the documentation of the symbol, this function was provided.
If {\tt INFO-TYPE} is ``{\tt :documentation}'', then a string is returned
which is the string used when defining {\tt SYMBOL}.
If no documentation is found, {\em nil} is returned.
If {\tt INFO-TYPE} is ``{\tt :type}'', then one of
{\em relation-class}, {\em function}, {\em production},
{\em world}, {\em instance}
is returned if the {\tt SYMBOL} is determined to be that type,
else {\em nil} is returned.
The default for {\tt INFO-TYPE} is ``{\tt :type}''.
\sline
EXAMPLE:\\
\vspace{-0.5in}
\asisblock{
(query-info intpower :documentation)
}
returns
\asisblock{
``Function which returns X to the power of Y.
Where Y is assumed Integer.''
}
while
\asisblock{
(query-info child)
}
will return {\em relation-class}.
\pagebreak
\subsection{reset-knowledge-base}
\sline\vspace{-0.5in}
\asisblock{
RESET-KNOWLEDGE-BASE (MACRO):
}
\vspace{-0.5in}\sline
Resets the knowledge base, ie, clears all knowledge in existence and
re-assert those set of things which \ttonto will assert as the primitive to
build from.
The set of things may include the pre-defined {\bf Second Order Keywords}
(see section to follow) and their definitions and the primitive class object
{\tt thing} which should be the most primitive class object.
This is a necessary bootstrap since all subsequent class and relation
definition would need some way of organizing the hierarchy.
It may also perform some initial function/method definitions if these are
required.
In general, the command brings the system to a stage where loading of the
knowledge base may be performed afresh reasonably.
The user may, therefore, after using this command, assume that there is a
most primitive {\tt thing} which is the ground class, some provided
{\bf Second Order Keywords}, but other than that, a mostly empty knowledge
base.
\pagebreak
\section{Second Order Keywords}
For both relations and classes, one may utilize some second order keywords to
state in some abstract but simpler fashion the limitations of these
relations or classes or their ``relation'' to other relations or classes.
The \ttonto provides a set of such keywords. It is possible for the user to
define some more (see example under ``{\tt tellm}'').
The currently supported keywords are:
\begin{itemize}
\item (asymmetric R): ($\implies$ (R x y) (not (R y x)))
\item (symmetric R): ($\implies$ (R x y) (R y x))
\item (reflexive R): (R x x)
\item (irreflexive R): ($\implies$ (R x y) (not (= x y)))
\item (weak-transitive R): ($\implies$ (R x y) (R y z) (not (= x z)) (R x z))
\item (transitive R): ($\implies$ (R x y) (R y z) (R x z))
\item (single-valued R): ($\implies$ (R x y) (R x z) (= x z))
\item (closed-world R): ($\suffice$ (not (R @l)) (not (provable (R @l))))
\item (disjoint-covering R1 ... Rn):\\
(and ($\implies$ (R1 @l)
(and (not (R2 @l)) ... (not (Rn @l)))) ...)
\item (inverse R P): [RELATION ONLY]\\
($\equival$ (R x y) (P y x)) [Extensible to n-ary]
\item (subrelation R P): [RELATION ONLY]\\
($\implies$ (R @l) (P @l))
\item (domain R C): [RELATION ONLY]\\
($\implies$ (R x y) (C x))
\item (range R C): [RELATION ONLY]\\
($\implies$ (R x y) (C y))
\item (subclass R P): [CLASS ONLY]\\
($\implies$ (R x) (P x))
\end{itemize}
There was no reason that these were the specific set of Second Order
Keywords adopted. Some of them are undoubtedly useful, others were already
keywords in LOOM and we decided to adopt them as well for \ttonto so we may
take advantage of these keywords in LOOM.
\chapter{Possible Worlds and Sharing}
In this chapter, the word knowledge would be used to denote, in the case of
LBA, the set of rules and facts maintained, and, in the case of FBA, the
frames and the inheritances and other interconnections amongst these frames.
\section{Partitioning Knowledge Bases and Sharing}
In even most of the simplest knowledge base systems, there are provisions for
partitioning knowledges into ``partitions,'' ``theories,'' ``models,'' or
simply called ``knowledge-bases.''
And, of these, most provide some way for ``including'' one theory in another
so that one ``partition'' might utilize the knowledge and information of
another ``partition.''
Of the 2 systems that are representative for FBA and LBA (LOOM and Epikit
respectively), this is true.
A study of the idea of ``inclusion'' of knowledge bases which has thus far
been intuitively stated, in formal notation yields the following.
We shall use the triplet $\Psi = <G,W,R>$ to denote the entire knowledge base
in the system, which may or may not be partitioned.
$W$ is the set of all partitions.
$G$ will denote the current partition which the system is working in (the
``active'' partition so to speak), and $R$ an ``accessibility'' relation such
that $(u,w)\in R$ {\em iff} $w$ was included into $u$'s partition,
{\em ie}
that $u$ can access the knowledge held in $w$ (in some direct fashion).
For each $u\in W$, $uRu$, {\em ie} $R$ is reflexive.
This usage is in accordance to possible world notation.
We define, thus, similar to possible world semantics, the operator $\poss$ as
follows:
\[\entails\poss\psi\;\mbox{\em iff}\;(\exists w)\;GRw\;\andl\;w\entails\psi\]
Where $w\entails\psi$ means that $\psi$ is true in $w$, and
$w\proves\psi$ to mean that, given $w$, the system can conclude $\psi$.
Thus, the semantics which describe inclusion and the effect \ttonto expects
are:
\begin{itemize}
\item[P1:]\(\entails\psi\;\mbox{\em iff}\;\psi\in G\;\mbox{OR}\;\proves\psi\)
\item[P2:]\(\entails\neg\psi\;\mbox{\em iff}\;
\neg\psi\in G\;\mbox{OR}\;\proves\neg\psi\)
\item[P3:]\(\entails(\psi\andl\phi)\;\mbox{\em iff}\;
\entails\psi\;\mbox{AND}\;\entails\phi\)
\item[A1:]\(\entails\poss\psi\implies\psi\)
\item[A2:]\(\entails(\poss\psi\;\andl\;\poss(\psi\implies\phi))
\implies\poss\phi\)
\item[R1:] from $\proves\psi$ and $\proves\psi\implies\phi$ infer $\proves\phi$.
\end{itemize}
This closely parodies the Kripke's possible world semantics, except for the
use of the $\poss$ instead of the $\nec$ operator.
The consequences of the definitions are:
\begin{itemize}
\item
Where we need to prove $\psi$, we will attempt to prove it first in the
current world, where it fails, we shall try to prove it via it's accessible
worlds.
\item
In trying to prove $\psi$ in the accessible worlds, wherein we encounter the
rule $\entails\phi\implies\psi$, we will attempt to prove $\phi$ from the
current world again.
\item
This may be recursively done.
\item
It may be possible to conclude both $\psi$ and $\neg\psi$ so long as
$\entails\poss^{n}\psi$ some $n$ and
$\entails\poss^{m}\neg\psi$ some $m$.\footnote{$\poss^{m}$ is the $\poss$
operator applied $m$ times.}
\item
Because of the order and direction of search, the ``nearest'' results and
rules will be utilized before the further ones.
This behaviour is inherently conducive to refinement down the children, since
the more refined results will be utilized.
\end{itemize}
The last item makes the entire ``inclusion'' method fragile, since to ensure
that the knowledge base does not have a contradiction (both proving $\psi$
and $\neg\psi$), none of the included partitions may contradict any other
partition.
This method of doing possible worlds is thus limited, but it is still an
important and useful mechanism to have and model.
\section{Dimensions}
In the building of possible worlds, be it for simulation or because it is
part of the knowledge that these ``possibilities'' exist parallel to ours if
only in our minds for analysis, it is recognized that there is a large
base of knowledge that is shared across some ``possibilities'' and other sets
which are shared across another set, where the intersection of these may be
one or several worlds.
It was thought interesting to analyze the pattern of sharing,\footnote{the
sharing here is the sharing of some facts inside of a system across
partitions and different thus from sharing entire knowledge bases between
users} and with the help of the DME project, the following first
approximations were concluded:
\begin{itemize}
\item
If we consider each state or knowledge base that is analyzed that is
``consistent'' and ``complete'' for the purpose of which the knowledge base
was produced as a world, it is hardly true that the entire world's knowledge
is shared.
\item
Of each world, there are some subset of knowledge which is shared amongst
some worlds and some other subset which are shared amongst yet others.
If we call the world which is included the parent world, and the other the
child world ({\em ie} the child world can see some part of the parent world),
we may analyze this as there being several types of parent-child branches,
with the particular subset being shared defining the type of branching.
\item
Sharing is sometimes not pure copying since it is often that the subsequent
sharing would add more facts to which may be shared by other worlds to
follow. Using the terminology developed in the previous point, we may state
that each child may choose to refine and add onto the part that it shares
with it's parent before passing it down to its child.
\end{itemize}
With regards to the fact that the world is subdivided into those which are
shared along each branch and that the branches normally correspond to the
``dimension'' (time dimension, possibility dimension and some such), we so
name these subsets.
These dimensions then are the portions of a world which is shareable by other
dimensions in other worlds.
The information that is shared must be able to function under the fragile
conditions specified in the previous section,
{\em ie} that it is not possible to both prove $\psi$ and $\neg\psi$ in any
2 worlds ``accessible'' from any world.
The limitation implies an inability to deal properly with nonmonotonicity via
this inclusion mechanism, except via non-inclusion ({\em ie} the parts which
contradict each other should thus not be placed in the partition), but is
still a useful mechanism.
It has a well defined formalism, and, given the capability to be ``in'' any
particular partition, one may control the efficiency of search by guiding and
directing the parents and ancestors to search.
The order of search is current world/dimension, the parents are searched
according to the order of inclusion. A somewhat ``depth-first'' nature is
thus duplicated.
Thus, utilizing this particular nature, one may direct the direction of
search across these worlds and dimensions.
Therefore, a world then is a knowledge base which may be partitioned into
dimensions where each dimension may be shared and may share the knowledge of
another dimension(s) from other world(s). These worlds are thus
``dimension accessible'' from this world and $R$ is the
``dimension accessibility'' relation.
The knowledge shared may be refined down the hierarchy but may not be
contradicted.
\section{Possible World Operators}
Unfortunately, the implication of the previous section is that there is no
possible world operator which works across these worlds in \ttonto as yet.
Therefore, \onto may choose to adopt yet another keyword, the keyword
{\bf true\_in} to achieve that.
The suggested syntax for the {\bf true\_in} operator is
\asisblock{
(true_in (<type> <accessibility reln>) <onto logic sentence>)
}
In as much as {\bf KIF} seems to wish to avoid this second order like
sentence, the ``expanded'' form might be used for the {\tt <onto logic
sentence>} portion of this syntax\footnote{for an example of the ``expanded''
form refer to the form inside the {\bf KIF} {\bf true} keyword in the example
in the discussion on the command {\bf tellm}}, thus the following may appear
in a knowledge base:
\asisblock{
(<= (= time (1+ \$t))
(true_in (necessarily backward) (list '= 'time \$t)))
}
Thus, {\tt type} may be one of {\tt necessary}, {\tt possibly} or a possible
world operator deemed necessary.
And the accessibility relation would denote the graph to which the worlds are
linked.\footnote{To achieve this, one may need to define a $(accessible\; R\;
W_1\; W_2)$ type of relation as well, which states that $W_1$ may access
$W_2$ via the accessibility relation $R$}
In the given example, it states that utilizing the backward accessibility
relation, if all the values of {\tt time} of the previous worlds is
{\tt \$t}, then this world must be the world at time {\tt \$t+1}.
Currently, it is possible to utilize a production to achieve some subset of
such behavior ({\em ie} define a specialize {\bf true\_in} operator), but that
is an application of production that is, at best, temporary, if not a
perversion.
Thus, \ttonto (along with {\bf KIF} and several others) does not have a good
notation for possible world operator, and the {\bf true\_in} operator so
suggested is primitive but adequate for now, but is as yet unimplemented nor
supported. This should be the next urgent step in the continued \ttontons.
\section{World Commands}
There are several world related commands available in the \ttontons.
However, these will probably be changed to accommodate the new ideas better,
and so will not be included here.
Again, the online documentation should provide adequate guide.
The commands available to date are
{\bf define-world},
{\bf perform-in-world},
{\bf perform-local-world},
{\bf perform-switch-world}, and
{\bf query-find-world}.
The functional dual of these are named as is similar to the other commands.
\chapter{Conclusion}
Again, it is stressed that \ttonto is a first attempt implementation of which
we are sure will contain misconceptions, mistranslations or other such.
However, the basic premise and idea, the \onto is sound and an important one.
Therefore, where in there is a failure or incompletion in the part of the
\ttontons, let the corrections be made and argued.
Where in there are refinements and conceptual changes needed for \ontons, let
the pages burn.
There are still several issues and items which should have been included and
discussed, but unfortunately, time constraints are upper most at this moment,
and it is hoped that this be a draft for a better document to come.
The forge is ready, the sword unfinished, may the first hammer hit be
resounding.
\appendix
\chapter{Acknowledgements}
My sincere thanks to Professor Tom Gruber for allowing me the chance to
undertake such a task and to provide numerous hours of refinement on my crude
ideas. Thanks also to James Rice who provided the bulk of support in the
implementation that is \ttontons, without whom \ttonto would have probably
been an unfathomable mess.
My gratitude also to Yumi Iwasaki, Low Chee Meng, Alon Y. Levy who provided
information and critique essential to my constant work.
Lastly, my appreciation goes to Darlene M Gong, whose mental support and
incessant care made life bearable and allowed me to push on.
\end{document}