KIF: new version of KIF-Core

[Michael Gruninger]

Chris Menzel wrote:

> Michael,
>
> Here are some comments on the new version.
>
> Section 1.1
>
> > * The language provides for the representation of knowledge about
> >   knowledge.
>
> This might be a bit misleading, since this is not true of KIF-core (or
> whatever we are calling the basic language).

This statement is in clause 1.1, and hence applies to the standard as a
whole.
The scope of KIF-Core is stated in clause 1.2

>
>
> Section 1.2
>
> I suggest beginning:
>
>   Part 1 of KIF specifies the syntax and semantics of a
>   first-order language with equality.  This language consits of ...

Sounds good.

>
>
> Section 3
>
> CONSISTENCY AND PROVABILITY
>
> I suggest defining consistency for theories:
>
>   A KIF theory T is consistent if and only if there is no sentence
>   A such that both A and (not A) are provable from T.

Right; this definition was inadvertantly left out ...

>
>
> One can then define the consistency of a sentence A with T in terms of
> the consistency of T U {A}.  Note that the notion of a theory needs to
> be introduced.  I suggest that you use the current definition of a module,
> viz.,
>
>   A KIF theory is a set of KIF sentences,
>
> and that all occurrences of "module" in this section be changed to
> "theory".

If we really are going to use the term "module" as a set of KIF sentences,
then we should replace all appearances of "theory" with "module",
and perhaps add a note that the traditional use of "theory" in mathematical
logic is equivalent to the use of "module" in KIF.

>
>
> Provability also needs some tightening up:
>
>   A proof (in a given namespace [see below]) is a finite sequence of
>   sentences G_1, ..., G_n (of that namespace) such that, for every i,
>   0<i<n+1, G_i is either a logical axiom, a member of T, or follows from
>   sentences occurring earlier than G_i in the sequence by a rule of
>   inference.
>
>   A sentence F is provable from a KIF theory T (in a given namespace)
>   iff there is proof (in that namespace) whose last element is F.
>
> The rules of inference for KIF can then be stated in the form "F follows
> from G_1, ..., and G_m" in order to comport with the above form (e.g.,
> "F follows from G and (implies G F)".  In fact, you might add the term
> "Rule of Inference" to the list of definitions here, where a RoI is a
> metalinguistic statement of the form "F follows from G_1, ..., and G_m",
> where "F" and the "G_i" are metavariables ranging over KIF sentences (in
> a given namespace).

The whole notion of inference arises solely to characterize conformance of
an application to KIF. The KIF standard only specifies the language and
semantics; there is no proof theory for KIF, and no rules of inference for
KIF
within the standard. The rules of inference belong to the software for which
we are evaluating conformance. In particular, the software is conformant to
KIF if its rules of inference are sound with respect to the semantics of KIF.



>
>
> INFERENCE SYSTEM
>
> I think this definition is a bit too metaphorical, since no sentences
> are ever literally transformed into new ones.  How about defining an
> inference system for a given namespace simply as a set of rules of
> inference for that namespace?  Note that if allow for different
> inference systems, the above definitions of provability etc will have to
> be relativized to both namespaces and inference systems.

Along these lines, I liked Pat's refinement of my original idea, since not
every piece of software will have explicit rules of inference (e.g.
constraint
solvers). Rather, we want to constrain the behaviour of such software
with respect to the KIF semantics.

>
>
> VARIABLE ASSIGNMENTS
>
> It is possible to eliminate the notion of a variable assignment by
> simply treating variables like constants.  This makes for semantics that
> is rather simpler to state.  (This is how we do it in the IJCAI paper.)
> If you clobber these, be sure to eliminate reference to them in Section
> 4.

When you teach your logic course, do you teach your students about
variable assignments or about treating variables like constants?
I mention this because  First-Order KIF is only
different from the traditional mathematical logic that we teach in that
we have a more free syntax that allows relations to be arguments to
relations. I do not want to give the impression that KIF is some new
logic. This is the reason that I was reluctant about the whole idea of
the extension function, since it is a very different treatment than the
the traditional specification of structure. However, I can empathize
with your viewpoint that resorting to non-well-founded set theory
can also be considered to be a violation of the traditional account.
In the case of extension vs. non-well-founded sets, we can show
that there is an equivalence between the two semantics.
I would agree to replacing the notion of variable assignments
in the main text with the approach from the IJCAI paper if we
could show in the annex that this is equivalent to the traditional
treatment of variable assignments and the treatment of quantifiers.

>
>
> EXTENSION FUNCTION
>
> There is no definition for extension function, used later.
>
> Section 4 (and Section 6)
>
> Concomitant changes would be required in
> Section 6.  I'd be happy to revise that section so that it comports with
> this this suggestion (as well as a number of other niggling
> suggestions).
>
>

OK. Send me a rewrite of the section, and I'll incorporate it into the draft.

- michael