KIF: new version of KIF-Core

[Chris Menzel]

> There is an educational issue here. How much knowledge of logic do we
> assume in the reader? Many readers of the standard will not know much
> at all, and will be quite unfamiliar with notions of model theory.
> The original KIF document tried to be something of a tutorial as well
> as a technical spec, and fell between the stools to some extent. We
> have a similar problem.
>
> I would be willing to try drafting some 'explanatory' paragraphs here
> and there, kind of Model Theory for Dummies, as I have been doing
> this informally to W3C working groups now for about a year.

Sounds good to me.

> >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.
>
> ? Surely consistency should be a semantic matter, not a
> proof-theoretic one. A theory is consistent if it has a satisfying
> interpretation. We don't have a notion of provability, do we?

Well, we can make it so, but "consistency" usually refers to the proof
theoretic notion.  I defined it proof theoretically because that is how
the notion of "consistent with" was defined.  (Satisfiability is the
corresponding semantic notion, of course.)

> >  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.
>
> That is too restrictive. There are many other notions of 'proof' out
> there as well as this line-style notion of proof as a sequence of
> sentences (resolution proofs, natural deduction, Gentzen-sequents,
> probably others). There is nothing in KIF that requires any
> particular kind of proof theory and I think that we shouldn't
> accidentally impose one (particularly one that isnt mechanically
> feasible :-)

Well, fine, it was really meant (though I didn't say) to serve as an
example of style.  Also, let's not confuse the formal notion of proof
with implementations thereof.  But point taken.

> Either we should give a particular proof system for KIF, or we should
> leave it open.

Yeah, I was sort of confused about that in the last version.  There was
reference to inference systems and terms that required some notion of
proof, but it seemed like Michael was leaving things open.  It has to be
clear that that is what we are doing, however, and if we are going to have
terms that require a notion of proof, then we need some sort of general
clear characterization.

> I would argue strongly that we do not make any particular proof system
> part of the standard,

I agree.

> What we can say is simply that any inference system or process is
> required to be correct under the KIF semantics. That is, we leave it
> up to the designer of the proof system to say what counts as an
> inference, but we require only that it be valid, whatever it is.

If that will do, fine.

> >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.
>
> I agree this is the best way to do it.

Yay.

> It also handles the free-variable case without needing any further
> elaboration.

Correct.  Note also that the existing docuement doesn't even use variable
assignments.  These are typically used in the semantic clause for
quantification, but Michael opted for an approach that requires names for
every object, as noted in my comments, which is problematic.  As also
noted, I will be revising that section.

-chris