incomplete translations

Tom Gruber <gruber@HPP.Stanford.EDU>
Date: Wed, 18 May 1994 19:08:57 -0700 (PDT)
From: Tom Gruber <gruber@HPP.Stanford.EDU>
Sender: gruber@HPP.Stanford.EDU
Reply-To: gruber@HPP.Stanford.EDU
Subject: incomplete translations
To: ontolingua@HPP.Stanford.EDU
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>
Message-id: <XLView.769315196.7590.gruber@hpp-ssc-1>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; CHARSET=US-ASCII
There are two kinds of translation problems we're talking about here
(<9405181525.AA20985@e51-007-3.MIT.EDU> <2978272259-9666234@KSL-EXP-35>).

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 
(http://ksl-web.stanford.edu/knowledge-sharing/papers/README.html#reversible-grammars).
"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 
type checking).

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.

tom

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...