Re: SUO: RE: A disclaimer about 'new KIF'
>John and Pat:
>
>This is just the sort of discussion which I should like to see more of, and
>which I consider essential to achieving clarity in a SUO.
>
>However, although I cannot tell with certainly, I think that you may be
>discussing at cross purposes, since John refers to some utilization of a
>hierarchy of meta-languages, while Pat speaks only of the expressiveness of
>'sorted FOL'.
>
>Clarification?
I will try. Background: part of the motivation for a 'new KIF' was a
perception that KIF, by trying to be aqll things to all mean, was
rather a complex and awkward beast, and that a stripped-down version
might be of greater utility. So the 'newKIF' is being designed to
have a 'core' which is as simple as possible, and several
'extensions' on top of the core which are kind of optional. The core
is now pretty well understood, and it will be similar to KIF 3.0 but
with a simpler syntax and a more powerful semantics, and will allow
superficially "higher-order" operations like quantifying over
relations and functions. However, it will not actually be
higher-order. (It is equivalent to a sublanguage of Lw1w which I
think is compact, but havnt quite proved this yet.) The extensions
are somewhat murkier than the core, but two of them that have been
fairly well identified are (1) a sorted extension, in which for
example argument 'sorts' for functions and relations can be specified
and will be checkable at parse time; and (2) a meta-extension, which
will have fully-fledged capabilities for describing its own syntax
(and the syntax of other languages).
Ive been working on the sorted extension but as far as I know nobody
has been seriously working on the meta-extension.
The sorted extension provides no actual logical expressivity beyond
the core; it only 'builds in' some of that expressivity into the
syntax, which many people find convenient. The meta-extension will
need a fully fledged mechanism for quasi-quotation and a
truth-predicate, at the very least, and probably some extra inference
rules for upward and downward reflection, so it will have a
considerably extended semantic theory which has not yet been fully
worked out. It ought to be capable of describing meta-languages to
any depth,in principle, though I imagine that it would rapidly become
unworkable in practice beyond two metalevels.
However, none of these will be genuinely higher-order. All extensions
of the language will be compact and have finite axiomatisations, and
will be efficiently implementable.
Hope this helps.
Pat Hayes
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes