November 30 - December 2, 2000
Participants:
Bill Andersen, Mike Genesereth, Michael Gruninger, Pat Hayes, Tom Ioerger, Chris Menzel, Adam Pease, John Sowa, Mark Stickel, Mike Uschold, Chris Welty, David Whitten
It was agreed that the SUO-KIF document will be used as the baseline, so that KIF-Core contains at least all of the features specified in the SUO-KIF document.
The following were some problems that were identified with SUO-KIF:
The group discussed the need for a syntactic mechanism for referring to namespaces, although there was concern that this could get bogged down in ontology management issues.
Consensus: There will be no commitment to namespaces, but that we will extend the BNF so that wordchar explicitly contains special alpha characters that can be used to identify namespaces.
Mike Genesereth raised earlier concerns regarding the introduction of features related to nonmonotonic reasoning, which was included in the KIF 3.0 document, but removed from subsequent drafts.
One proposal was to identify operators (such as unprovable, bagofall ) that people could use to specify nonmonotonic features. We would also provide syntax to allow people to incorporate new operators; however, within the standard, operators would be uninterpreted constructs.
Consensus: The group did not arrive at any consensus on this issue, although if they are included, they will belong to a new extension.
Action Item: Mike Genesereth will flesh out the requirements for nonmonotonic operators.
The introduction of a sorted extension to KIF is motivated by the following concerns:
The group agreed that KIF-Core should be unsorted.
After a great deal of discussion, there was still disagreement about the introduction of a Sorted KIF extension. The objections were primarily concerned with the danger of the balkanization of the standard, particularly when merging two ontologies in which one ontology uses only the unsorted Core while the other uses the Sorted extension. Another objection was that the declaration of sort information belongs more properly to an ontology rather than the language of KIF.
There was discussion concerning the declaration of sorts. Declaring sorts before using them could result in undesired behaviors. The sort hierarchy has to be set a priori, but you will get errors that you do not want, if the sort hierarchy is not set up correctly. E.g. variable ?x is a human, could be rejected by a parser if not yet delclared to be a subsort of animal. The problem is that in an open world, people will often be adding sorts and changing the hierarchy.
Among those who are proposing a Sorted KIF extension, there was agreement on the required features. Given the restricted quantifiers from the KIF-Core BNF, there is no change to the BNF of the Sorted KIF extension. However, the syntax for specifying sort information (i.e. sort signature) must be added. This would include new operators defsort, topsort , and subsort, as well as boolean operators on sorts (union, intersection, complement).
There was some disagreement about including the restricted quantification in KIF-Core. However, it was argued that restricted quantification provides a convenient syntax for users, as well as providing a hook to make it easy to link with the Sorted extension.
Action Items:
Pat Hayes will sketch out the syntax for sort declarations (as top-level forms that are not embedded in formulae). This will include a treatment of the interaction between sorting and having variables in the predicate position.
There is also a need to write a few notes on the semantics for the new grammatical constructs in the proposed Sorted KIF extension.
Undecided Issues?
Although these had earlier been eliminated in the first teleconference, Mike Genesereth urged that they be reintroduced as part of KIF-Core (as they are in the dpANS document). Although variadic relations can be included without sequence variables, Mike argued that they sequence variables provide a simple way of dealing with n-ary arguments and lists.
The following objections were raised against the introduction of sequence variables:
Consensus: The use of variadic relations was not contentious, but no consensus was reached on the introduction of sequence variables (although there was relatively strong support for their inclusion).
Action Item: Mike Genesereth will write a clear exposition of the semantics of sequence variables @l .
An example of this is
(<=> (symmetric ?R) (<=> (?R ?x ?y) (?R ?y ?x)))
It was agreed that this can be handled by saying that we are quantifying only over all relations in the domain of discourse.
An unresolved issue is the interaction between this feature and sorted languages.
Action Item: Chris Menzel will fully specify the semantics of this quantification.
The introduction of the MetaKIF is motivated by the following concerns:
The main discussion revolved around proposals for quote and the model theory of MetaKIF. The original treatment of quote from KIF 3.0 and the dpANS document (which we shall refer to in these notes as structured quote), was based on the use of lists and the restriction to finite lists in particular.
There were three proposals for handling quote:
Mike Genesereth described two motivations for his structured quote approach. KIF originally had an abstract syntax (graphs), which was linearized into strings; using Menzel's character string quote would be a bias towards a particular linearization. In addition, structured quote assists in the implementation of reflection principles.
Action Items:
Mike Genesereth will tidy up his proposal for quote and bring it line with its stated semantics. Chris Menzel will also flesh out the model theory of his approach. We will then evaluate these two proposals on the basis of their model theories. Also, Mike Genesereth will provide examples illustrating why implicit quoting is insufficient.
The proposal here was to adopt wtr within the MetaKIF extension.
Consensus: We will leave this issue open for now, altough some truth predicate is required, particularly to write axiom schemata.
There were no technical issues here. The group agreed to incorporate a DTD for the KIF BNF as an annex to the standards document.
The original complexity around these constructs arose from the distinctions between conservative and partial definitions in the KIF 3.0 document, which are not present in the dpANS document.
The proposal was to introduce a single def construct in the MetaKIF extension. We still need a BNF for this construct.
John Sowa had earlier proposed the addition of an assert operator. The group felt that the functionality of such an operator could be captured by wtr.
This discussion is motivated by the question of whether or not the following expression should be syntactically legal:
(P (P P) P)so that the same string is referring to a predicate, function, and constant.
The proposal was that there be no punning allowed. To prevent this, functions and predicates must be disjoint in the BNF. We will create non-terminals called pred and func, with the same definition as definition for word. We will state that no pred shall have same characters as a word, and no func shall have same characters as a word. One drawback is that it does not allow a complete BNF.