Propositions and Knowledge Interchange

macgregor@ISI.EDU
Message-id: <199402151828.AA23509@quark.isi.edu>
X-Sender: macgreg@quark.isi.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 15 Feb 1994 11:05:19 -0800
To: cg@cs.umn.edu, interlingua@ISI.EDU
From: macgregor@ISI.EDU
Subject: Propositions and Knowledge Interchange

John Sowa has just described what looks like a pretty good definition
of a proposition, i.e., I have no problem with the procedure that he
proposes to define equivalence classes of sentences. However, for the
purposes of defining an interchange format, I would be satisfied with
much less. All I really need is that some *notion* of proposition exists
in the interchange language/ontology. Suppose I want to translate from
language/system/kb A to language/system/kb B, and both have notions of
proposition built into them. Suppose that the axiomatization of
"proposition" is not identical in the two systems, but is similar "in
spirit", i.e., for the purposes of translation, I want propositions in
A to be translated into propositions in B.  What's missing in KIF for
me to make this translation is some means of identifying propositions
at the halfway point of the translation, when they are defined 
in KIF.

Suppose we add propositions to KIF, and adopt John's semantics. My
A-to-KIF translator may or may not pay attention to that semantics when
mapping propositions from A to KIF. Similarly, my KIF-to-B translator
may or may not pay attention to the KIF semantics of propositions. In
fact, there is an inverse relationship between how much will get
translated and how tightly coupled the translators are to the KIF
semantics. If only propositions that exactly match the KIF semantics
get translated as propositions, then in my example above, NONE of the
propositions in A will get translated into propositions in B.

The phenomenon of (partially) ignoring the KIF semantics already
happens in the case of definitions.  For example, a Loom definition
has different semantics from a KIF definition, and a CLASSIC
definition has semantics different from either.  That doesn't
prevent us from translating a Loom definition to a Classic definition,
since the translators written thus far don't pay any attention to
the KIF semantics.

So, from the standpoint of translating such things as definitions, types,
and propositions, it makes little difference which semantics KIF
chooses to specify.  The important thing is that each of these 
is given a standard "name" that a translator can look to when translating
in and out of KIF.  If that name has an elegant semantics associated
with it, so much the better.

I can't imagine a standard being approved that doesn't specify a semantics.
But for practical purposes, it matters little what that semantics happens
to be.

- Bob


Robert M. MacGregor                                     macgregor@isi.edu
USC/ISI, 4676 Admiralty Way, Marina del Rey, CA 90292      (310) 822-1511