Minutes for KIF Standardization Meeting

Pat Hayes, Chris Menzel, Adam Pease, Mark Stickel, Mike Uschold, Chris Welty, Michael Gruninger

Discussion

1. Organize KIF into a KIF-Core and a set of modules.

   In general, these issues raised a number of different points concerning the nature of languages, lexicons (signatures), and theories.

   Adam emphasized the need to distinguish the language of KIF from ontologies that can be written in KIF.

   The discussion centered on what it meant for something to be an ``extension'' of KIF-Core. Chris Menzel identified two approaches to defining extensions to the language:

   • KIF-Core contains only one nonlogical symbol (=); all others are introduced and axiomatized in extensions;
   • The language of KIF-Core includes all possible relation symbols, but only equality is axiomatized in the Core
   Pat raised the issue of how to extend the language when building ontologies. In particular, what is the syntax for declarations for new symbols in the language?

   Chris responded by proposing that we define the notion of the language of a "KIF theory", which would include a possibly empty set of predicates (except for =), a possibly empty set of function symbols, and a possibly empty set of constant symbols.

   The fundamental issue here is:

   What is the language of KIF, and how do we ensure extensibility?

   Adam saw three aspects to the language:

   • BNF grammar
   • axioms for the lexicon i.e. terminals of the grammar
   • ontologies/theories

2. Proposed extensions to KIF-Core

   Adam expressed concerns that the modular organization of KIF could lead to the balkanization of the standard. (Editor's note: This is my wording, but I believe that it captures the danger that whenever contentious issues arise, the proposed options will be treated as different extensions rather than be resolved in a unified manner within the standard.) The following general principle was proposed:

   For any extension, we should be able to "back-translate" into the KIF-Core.

3. Omit variadic relations and functions

   The group agreed to adopt this proposal.

4. Omit sequence quantification

   The group agreed to adopt this proposal.

5. Eliminate the identification of expressions with lists

   The group agreed to adopt this proposal.

6. Allow case-sensitive identifier names

   The group agreed to adopt this proposal.

7. Introduce a sorted language definition

   The discussion of this feature revolved around whether it should be included in KIF-Core, and also on how sorts should be incorporated into the syntax. One proposal was that sorts could be a grammatical extension to KIF-Core; the problem is that sorts complicate the grammar.

   Mark Stickel and Pat Hayes both stressed the need of an additional specification of the grammar for a sorted language rather than relying on the mapping between sorted and nonsorted language. In particular, one can take a non-well-formed formula in a sorted language and map it into a well-formed formula in a nonsorted language.

   Chris Menzel had earlier proposed an approach to sorted languages based on Enderton. However, it was felt that this approach is too simplistic for KIF.

8. Simplify and reorganize quotation

   The group agreed to table this issue for the workshop.

9. Retain the use of the truth predicate wtr, possibly within the Metatheory Extension.

   Editor's note: I can't remember what we said here ...

10. Change the syntax for definitional forms

    The group agreed to adopt this proposal, although no new syntactic constructs were proposed. Pat stressed the need for some syntactic mechanism for pointing out definitions without the logical weight of the definitional forms in the current KIF documents.

11. Introduce lambda expressions

    The group agreed to table this issue for the workshop.

12. Allow general terms, including variables, to occur in the first position of expressions (i.e. relations and functions need not be constant symbols.)

    Editor's note: I can't remember what we said here ...

13. Introduce expressions (not just KIF expressions, but arbitrary expressions) as first-class entities, distinct from lists, and have a reasonably powerful syntax-description ability using the language to express BNF directly.

    The group agreed tht we need the ability to describe languages and their syntax. Ontologies can be written using this language extension; the original KIF Metatheory would be one such ontology.

    This feature (together with quotation) will be necessary to specify axiom schemata

14. Integrate a modern class-inheritance mechanism into the syntax.

    This issue will be tabled either to a later meeting or the workshop.

Action Items

1. Chris Menzel will identify options for addressing the issue of "What is a language?"
2. Identification of options for sorted languages. (I can't remember who was going to do this).