incomplete translationsTom Gruber <gruber@HPP.Stanford.EDU>
Date: Wed, 18 May 1994 19:08:57 -0700 (PDT)
From: Tom Gruber <gruber@HPP.Stanford.EDU>
Subject: incomplete translations
cc: Cheng Hian GOH <chgoh@MIT.EDU>, James Rice <Rice@HPP.Stanford.EDU>
In-reply-to: James Rice's message of Wed, 18 May 94 10:50:59 PDT: <2978272259-9666234@KSL-EXP-35>
Content-Type: TEXT/PLAIN; CHARSET=US-ASCII
There are two kinds of translation problems we're talking about here
First, KIF is more expressive than most implemented representation systems, and
that is by design (see paper to come out next week in KR94 by van Baalen and
Fikes that explains why this is a requirement
"more expressive" means that there will be some axioms in the KIF
theory that cannot be stated in the target language. Our previous
implementations issued a warning and threw such axioms away. The new release
attempts to add them on an "OTHER-AXIOMS" slot as quoted expressions. This
allows for reversability in translation.
There are many kinds of axioms that can't be expressed in Loom, and that's to
be understood. As long as we're talking about monotonic stuff, a subset of the
ontology will still be internally coherent and consistent with the complete
ontology. So this is acceptable for many purposes (i.e., for those kinds of
inferences that Loom and most frame systems can perform, such as slot value
The second translation problem has to do with context-dependent or procedural
semantics for expressions in the target representation language. Sometimes,
forms that are perfectly legal _syntacticly_ may not make the target system
happy. For example, Loom will throw you in the debugger if you mention some
constants in certain contexts before their definitions have been processed. In
this case, Loom's language (not grammar) insists on an ordering in the
definitions, and a completeness of the T-box before using the A-box (KIF
doesn't have these constraints). This is the class of problem that kept us
from releasing a bug-free Loom translator.
We met with the chief designer/developer of Loom, and together we identified
some fixes to Loom that might help overcome some of these problems; we've also
developed workaround strategies from Ontolingua. Our goal is to at least get
the Ontolinuga/Loom combination to produce files that Loom can load without
errors that put you in the debugger.
Nonetheless, there is no guarantee in an ontology about which _inferences_ are
to be performed. That is a different issue than the semantics of the
definitions in an ontology, which are independent of inference mechanism or
proof procedure. This is what Rice was referring to when he said that if you
want to use the full power of KIF you will need something more like a theorem
prover <2978272259-9666234@KSL-EXP-35>. For example, I doubt that Loom can
prove the dimensional equivalence of quantity expressions, even if the complete
axiomatization of that domain is translated into Loom.
However, we still write the axioms that these systems can't do inference over,
because the axioms are an excellent way to communicate our meaning and because
there are _some_ tools (that we wouldn't embed in applications) that _can_ do
inference over the theories (e.g., for analysis purposes, or to prove
conformance). We can build agents that may only care about the class
hierarchy; if so, ontolingua can extract the class hierarchy axioms from all
the rest and present it in a canonical form for translation. "All the rest"
then act like comments on the code ;-).
I hope this helps. And I hope we will be able to produce an adequate Loom
translator for the final release.
P.S. If all you want is the class hiearchy and slot inheritance, you can use
the generic frame implementation in Ontolingua, with the GFP API. If you want
it in C, we'll be releasing a CLIPS translator soon...