The following is an exhaustive chronological list of decisions made by the KIF Ad Hoc Group.
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.
(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.
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
(*) 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:
(*) 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