Re: kif
Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Date: Wed, 15 Dec 93 19:08:34 PST
From: Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Message-id: <9312160308.AA00993@t.uoregon.edu>
To: genesereth@cs.stanford.edu, interlingua@ISI.EDU
Subject: Re: kif
Cc: perlis@cs.umd.edu
Ho ho! (A little bit of Xmas spirit, there.) Mike's message
contains a variety of things that seem either interesting or
humorous.
Into this argument was injected the point that, while nonstandard
models of things like transitive closure are a problem for knowledge
REPRESENTATION, they are irrelevant to knowledge INTERCHANGE. The
same conclusions can be drawn whichever semantics one chooses!
In other words, the semantics are independent of the semantics. I
cannot imagine a context in which such a statement is defensible.
The problem of metalevel paradoxes is also mentioned in the
specification, though in this case the discussion is even briefer.
There are numerous ways to eliminate the metalevel paradoxes
popularized by Montague. Kripke (Journal of Philosophy 1975) gives an
axiomatic approach based on Kleene's strong three-valued logic.
Feferman (Journal of Symbolic Logic 1984) provides a simpler
axiomatization. Feferman's version is essentially equivalent to the
one described by Perlis (AIJ 1986). Perlis's version is the one used
in KIF. Perlis's article on self-reference proves that the axiom
schema true(p)<=>p* is consistent with any theory not containing any
occurrences of the true predicate. In other words, the semantics is
not paradoxical, though one can write sentences that turn out to be
false.
At last! Actual references to material in the published literature.
(There are no references at all in the KIF document I ftp'ed from
Stanford earlier today.)
Perlis had no paper in AIJ in 1986, so I will assume that the 1985
paper is meant. The Perlis paper adds the axiom
True("A") <-> (A)* (1)
where * encapsulates a trick developed by Glymour for avoiding
paradox. There are several things to note here:
1. This is *NOT* the axiom appearing in the standards document.
Equation (9.31) in the KIF standard is
(<=> (true phi) phi*) (2)
Note the absence of quotes in this axiom relative to Perlis' (1); I
believe that this use-mention confusion invalidates any attempt to use
Perlis' results to demonstrate the consistency of KIF.
2. The notion of "true" that Perlis uses is not nearly so broad as
the KIF folks would have us think. Specifically, True(x) means that x
"can be reduced to formulas not involving "True"." [Perlis, p.310]
which limits substantially the universality suggested in the KIF
document itself.
3. Perlis says [p.306] after lengthy argument that "Because of these
[previously described] difficulties the approach of levels [i.e.,
hierarchies] appears too restrictive for AI in general." Yet we have
just seen a lengthy message from John Sowa explaining that the whole
reason the KIF approach works is *because* it is hierarchical. Now
Genesereth explains that it works because it is equivalent to Perlis'
non-hierarchical method although, as we saw in (1) and (2) above, that
equivalence is bogus.
Those interested in these isues should look at the book ``Truth and
Modality for Knowledge Representation'' by Ray Turner (MIT Press),
especially his proof of the equivalence of the KIF axiomatization to a
variation of that described by Kleene.
I'm not sure how to parse this. Surely the KIF approach, which both
is and is not equivalent to Perlis' (as seen above), can't be
equivalent to Kripke's Kleene-based approach, since Perlis and Kripke
are not equivalent (see Perlis p.310, where he notes that Kripke lacks
a law of the excluded middle). But Mike's paragraph seems to be
saying that KIF is only *almost* equivalent to Kripke/Kleene, which I
guess means that it both is and is not equivalent to Kripke/Kleene.
To summarize, we can be pretty well assured that the basic APPROACH
taken in KIF is safe from paradox. The semantic basis for KIF has
been documented, reviewed, and published in the mathematical and ai
literature for years.
KIF both is and is not equivalent to Perlis, and also both is and is
not equivalent to Kripke/Kleene. Kripke/Kleene and Perlis are not
equivalent to one another, but they are both consistent. It follows
>From this that KIF is safe from paradox?
In conclusion, I would like to point out that the members of the
Interlingua committee have done a lot of work on this spec, as have
the outside reviewers. And more work is being done all of the time --
to refine the language, to document it, and to use it. This is no
slapdash effort.
Welcome to the 90's. What matters is not that the claims made about
the language are correct or independently verified, but that a lot of
hard work went into its development.
I am personally gratified to see so much discussion on the mailing
list. However, I would like to encourage us to concentrate on
constructive criticism. The best questions are those based on uses of
the language, accompanied by specific examples (like Lehman's list).
The best kinds of criticisms are those that are based on proven
difficulties, together with specific alternatives in the spirit of the
language (like Gruber's criticisms eraly on in the effort and Sowa's
more recent recommendations for extended quantifiers).
Criticisms based on counterexamples are not the only ones generally
made in academic circles. Are comments pointing out that the KIF
claims are based on misapplications of previous work really not
welcome?
Matt Ginsberg