Knowledge Interchange Format (KIF)

Decisions


The following is an exhaustive chronological list of decisions made by the KIF Ad Hoc Group.

95-1: Charge to the Ad Hoc Group

The goal of the KIF Ad Hoc Group is to produce a draft proposal for an American National Standard for KIF. The starting point for this effort is to be the Reference Manual for KIF Version 3 produced under the auspices of the ARPA Knowledge Sharing Effort. The scope of the initial draft is to be first-order KIF with extensions to handle syntactic metaknowledge.

Note that this means no higher order constructs, no modals, and no nonmonotonic constructs in this version. X3T2 recognizes that it may eventually be necessary to include additional constructs and would like us to design the initial version in a way that would facilitate such extensions in the future. Furthermore, there is an interest in seeing us investigate what would be needed for such extensions so long as it does not interfere with our primary work.


95-2: Procedural Matters

(1) It was agreed that all substantive modifications to the the standard would be treated in two phases. The first would be a discussion in an open electronic forum, i.e. by email or newsgroup, for a fixed period of time. In the second phase, the editor would summarize this discussion for the ad hoc group; the members would then discuss it among themselves and vote.

(2) It was agreed that the editor would maintain on the web the working document for the standard, the text of all discussions, a summary of all decisions, the rationale for those decisions.

(3) It was agreed that we need to promote KIF through the publication of documents that are more accessible than the standard, e.g. a general introduction to kif and overviews in the AI Magazine and other popular magazines.

(4) It was agreed that we should participate in liaison activities with related efforts, notably the work in X3T2 on CSMF, the work of X3J21 on Object Z, and possibly SC7/WG11 on CDIF.

(5) International Standardization. Jim Fulton put us in touch with Pete Eirich of SC7/WG11 and we have sent a copy of our working draft. There is a chance that that group might be willing to be the vehicle for producing a Draft International Standard for KIF through ISO.


95-3: Starting Point

As mentioned above, the starting point for the effort is to be the Reference Manual for KIF Version 3. However, the AHG agreed that we should start with a modified version of this manual for two reasons: (1) to reduce it to the first order subset mandated in our charge, (2) to get it into proper form for a standard, and (3) to incorporate some pending changes to the document accumulated over the last two years.

I have made these changes to the manual and placed a copy on the web. This document is, therefore, the starting point for our work. The following paragraphs summarize the changes to the Version 3 Manual.

(*) Elimination of nonmonotonic constructs. Deletion of operators =>> and <<= and consis from the syntax, deletion of section on nonmonotonic entailment, deletion of chapter on nonmonotonic knowledge.

(*) BNF Syntax to replace current reference to the LISP reader. Extension of syntax to handle bit blocks, needed for incorporation of audio, video, images, etc. (In short, #nQcharacter^n allows for transmission of characters without the need for quoting characters.)

(*) Simplification of truth predicate TRUTH to WTR (weakly true). As you know, a truth predicate with semantics (<=> (TRUTH 'p) p) leads to paradoxes. Therefeore, the semantics of TRUTH was defined via the axiom schema (<=> (TRUTH 'p) p*) where p* is a variant of p in which (NOT (TRUTH 'q)) becomes (TRUTH '(NOT q)). Kripke, Feferman, and Gilmore and also Perlis show that this construct avoids paradoxes. Unfortunately, it is difficult to predict the truth value of complicated cases of this and it is difficult to implement. Since the purpose of the truth predicate in KIF is primarily to allow the codification of axiom schemata, we do not need anything nearly so complicated. So, we have decided to go with a simpler version WTR, which satisfies (<=> (WTR 'p) p) where p is free of WTR and otherwise is false. This is also free from paradoxes; it is predictable; and it is implementable.

(*) Addition of syntax to allow for user-definable operators. It is generally acknowledged that we need tohave an extensible operator set. Such operators need to be syntactically distinguishable from constants. It was agreed to reserve all words of the form .alphanumeric. to this purpose. A system receiving an expression containing such an operator would not be permitted to do any deduction that would substitute into that expression without appropriate metalevel axioms sanctioning such substitutions. Using WTR it would be possible to define these new operators.

(*) Conversion of support for sets, function, relations from core constructs to ontologies. Given an extensible set of operators and a way of defining their semantics as metalevel axioms, it was decided that support for arbitrary sets, functions, and relations (as entities in universe of discourse) would be eliminated from the core of KIF. The current constructs would be defined within ontologies. Two reasons for this. (1) The lack of unanimous satisfaction with the von Neumann Godel Bernays set theory. These things were in core ONLY because previously there was no way to define them in an ontology because ofthe inability to define new operators (an inability now gone). (2) The second reason is the off chance that work on second order kif will proceed rapidly enough that these matters could be dealt with at the second order where they properly belong. Note that the VERY POPULAR frames ontology depends on these things heavily. Moving them out of the core does not hurt these efforts. However, it impedes our efforts to move the frames ontology into the core. Fortunately, a look at the frame ontology reveals that it can be done by reifying slots and adding a corresponding VALUE relation; there is no need for the full power of the VBG set theory.

(*) Typed quantifiers. This issue was aired on the mailing list many months ago, at the prompting of John Sowa and evoked no substantial complaints. The idea is simpy to allow syntactic sugar. Example:

(FORALL ((?n INTEGER)) (NUMBER ?n)) stands for (FORALL (?n) (=> (INTEGER ?n) (NUMBER ?n))) (*) Frames. There has been great demand for inclusion of basic vocabulary of frames. We will include some of this in the core.

(*) Strings. Ditto support for strings, mostly to define the surface syntax of computer languages.

(*) Definitions simplified. I have incorporated the simplification to support for definitions submitted by Richard Fikes last December.


Michael R. Genesereth , Stanford University, genesereth@cs.stanford.edu