X3T2 and KIF
genesereth@cs.stanford.edu (Michael R. Genesereth)
Date: Tue, 6 Jun 1995 18:48:08 -0700
Message-id: <199506070148.AA00446@Sunburn.Stanford.EDU>
To: cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu
From: genesereth@cs.stanford.edu (Michael R. Genesereth)
X-Sender: mrg@sunburn.stanford.edu
Subject: X3T2 and KIF
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
Folks,
Here is my first report on the ANSI X3T2 KIF ad hoc group. My apologies for
the delay in sending this, but the transition from arpa-run project to ANSI
project was delicate. I am not sure I have handled it well, but I cannot wait
any longer.
The good news is that we are now official. ANSI OMC has approved a project to
produce a dpANS (draft proposed American National Standard) for KIF and has
assigned the work to X3T2, the committee on Information Interchange. X3T2
handles things like ASN.1. To deal with the project, X3T2 has set up an Ad Hoc
Group on KIF; and this group convened for the first time at an X3T2 meeting in
Palo Alto this Spring. At that meeting, the adhoc group agreed on a number of
items. I summarize these for you in this note.
In future notes, I will go into more detail about our web presence (see
http://logic.stanford.edu/kif.html for a copy of the current version of the
manual), procedures for participation via email (address
kif@cs.stanford.edu), and procedures for joining X3T2 should you wish to do
that. (Note that there is no requirement to join X3T2 to participate in
the email discussion.)
CHARGE TO THE KIF AHG:
The goal of the KIF Ad Hoc Group is to produce a draft proposal for an American
National Standard for KIF in approximately one year. (After this, the approval
of the standard could go quickly or could take many years, at our discretion.)
The starting point for this effort is to be the Reference Manual for KIF Version
3.0 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.
****
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.
****
STARTING DOCUMENT
As mentioned above, the starting point for the effort is to be the Reference
Manual for KIF Version 3.0. 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.0 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, #<n>q<character>^n allows for transmission of <n> 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 'phi) phi) leads to
paradoxes. Therefeore, the semantics of TRUTH was defined via the axiom schema
(<=> (TRUTH 'phi) phi*) where phi* is a variant of phi in which (NOT (TRUTH
'psi)) becomes (TRUTH '(NOT psi)). 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 'phi) phi) where phi is free of WTR and otherwise is
false. This also feres 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 to have 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 of the
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. Stay tuned.
(*) Strings. Ditto support for strings, mostly to define the surface syntax of
computer languages. Stay tuned.
(*) Definitions simplified. I have incorporated the simplification to support
for definitions submitted by Richard Fikes last December.
****
ISSUES TO BE WORKED ON
Numerous issues were raised in the meeting and were placed on the agenda for
general email discussion. These include the following:
(*) Infix syntax option. Genesereth has agreed to distribute his infix variant
of KIF for general comment.
(*) Arithmetic. Should we define just for numeral-representable numbers or
should we offer axiomatizations.
(*) Ontology of procedures and processes
(*) Modal operators defined in ontologies using extensible operator syntax.
(*) Work on second order KIF
(*) Story on handling of nonmonotonic information.
(*) Relationship to contexts, names, indexicals
************************************************************************
Michael R. Genesereth genesereth@cs.stanford.edu
Computer Science Department 415-723-0324
Stanford University Fax: 415-725-7411
Stanford CA 94305 http://logic.stanford.edu/genesereth.html
************************************************************************