Re: kif

Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Date: Thu, 16 Dec 93 10:35:12 PST
From: Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Message-id: <9312161835.AA01234@t.uoregon.edu>
To: genesereth@cs.stanford.edu, ginsberg@cs.uoregon.edu
Subject: Re: kif
Cc: interlingua@ISI.EDU, perlis@cs.umd.edu

  
  Right you are in point out the typo in the current ersion of the kif spec. 
  The schema should read as follows:
  
  (<=> (true 'phi) phi*)

The KIF document, a self-proclaimed paragon of careful work and outside
reviewing, contains a single axiom giving the semantics of the metalevel
predicate True.  This axiom makes a use-mention error that invalidates
the approach, and the KIF author dismisses it as a "typo".

Even more interesting is the fact that this same "typo" appears
uniformly throughout Chapter 9 of the KIF document.  The sentential
arguments that Perlis is careful to quote throughout are not quoted
on the bottom of p.46; in fact, they are specifically *unquoted*
(using comma) in the middle of p.47.  Perhaps this is less a typo than
a misunderstanding of Perlis' approach itself.
  
  the axiom schema [is consistent] with any kb not containing true.
  This shows that it is not paradoxical.  ne can then add any statements
  containing true that are not themselves paradoxcal ...

In other words, the only guarantee that paradoxes are avoided is if
the user doesn't himself use the True predicate!  Beyond that, there
are no assurances whatsoever.  This is what Mike meant when he said
that we could "rest assured" that paradox was not an issue in KIF?

There is a real lesson here.  Perlis' work is not the final word on
self-reference in first-order languages; it is only one step along a
still incomplete path.  It always amazes me that the KIF folks are
prepared to standardize things that humans do not yet understand.

  I think I can safely say that the spirit of your note is not the
  constructive spirit I was advocating in my last paragraph.  Ho ho ho
  yourself, scroogy.

The existing KIF document is completely lacking in academic
credibility; suggesting that the methodology needs to be changed is
indeed a constructive -- and necessary -- step toward producing an
interlingua that the community at large should be prepared to consider
or to use.  If the goal, however, is simply to establish the
triumvirate of Fikes, Genesereth and Sowa as capable of making
progress by fiat, as somehow exempted from standard academic process,
I confess to having nothing positive to offer.

Rather than continue the dispute, though, it seems to me that we can
settle this fairly easily.  Why don't we simply send the KIF document
out for technical review by people who have not yet expressed strong
sentiments about it?  Natural suggestions would be Doyle, Israel,
Levesque or Perlis.  Perlis is presumably somewhat biased in favor
due to the inclusion of his work on quotation, and Israel expressed
concerns about the value of standards at KR-91.  I'd suggest Doyle and
Levesque, if they're willing to do it.

						Matt Ginsberg