KIF: Definitions in KIF

[pat hayes]

> > >I never claimed full compliance with KIF 3.  SNARK has its own
> > >input language and rules that usefully overlaps KIF.
> >
> > OK, fair enough, and I apologise for getting this wrong. But then it
> > can similarly 'overlap' ISO-KIF, so what is the problem? If you are
> > happy to not claim conformity, then your implementation need not
> > constrain the design of the language at all. Nobody is attempting to
> > force you to implement anything that you find uncomfortable.
>
>I would prefer to conform.  I'm just making the case that some
>features of the evolving KIF standard appear to cause problems for me.
>If features might cause problems, it is fair to consider whether those
>features need be present.  There are reasons to allow symbols to be
>used in both function and relation position.  I have reasons to not
>allow it, whether you respect them or not.

I respect them, but I think that we are disagreeing about what "allow" means.

>As noboby else seems to
>share my concern, I concede that the KIF standard will allow it,
>regardless of whether the feature is usually or usually not available
>in existing theorem provers and whether I'm willing to support it in
>mine.

That is very gracious of you. Also, it might be a good idea to be 
able to state a conformance category (level? whatever) which 
corresponds to the restriction you are comfortable with. On looking 
at the BNF I sent out recently I realise that it does not make such 
categorizations easy, and I will send out a revision to rectify this 
(Monday).

>
> > >As for using relation symbols as function symbols and as constant
> > >symbols, this not a feature of SNARK syntax.  SNARK has separate
> > >namespaces for relations, functions, propositions, and constants.
> > >SNARK does allow punning (although a warning is issued): J can be used
> > >as relation, function, and constant symbol with no semantic relation
> > >between them unless the user provides axioms for it.
> >
> > I consider this a bug rather than a feature, and I believe it gave
> > rise to some problems in HPKB as well.
>
>This wasn't my first choice either, but what you regard as a bug was
>relied upon by some axiom writers; this feature was motivated by the
>desire to import pre-existing theorem-proving problems written with
>that convention.  There certainly were problems for me and users when
>such different interpretations of input expressions are used.

OK, fair enough again. What this kind of experience suggests to me is 
that a fully functional KIF (even a fully functional SUO-KIF, in 
fact) should be able to state conventions like this in the language, 
so that one can assert that a module is written relying on some 
syntactic convention or restriction. We might take this example as a 
test case for designing the meta-language extension, in fact. A 
similar kind of requirement has surfaced in the DAML discussions, 
where it is widely accepted that the overall logic must be monotonic, 
but particular namespaces might rely on a closed-world assumption. 
What one needs is a general way to say of a particular namespace that 
it is 'closed'.

Pat

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes at ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes