Common Logic Standardization Meeting

Stanford University

March 21-22

Attendees

The meeting was attended, in whole or in part, by Michael Genesereth (host), Michael Gruninger (editor), Pat Hayes, John McCarthy, Chris Menzel, Adam Pease, John Sowa, Mark Stickel, and Charles White.

Merging KIF and CG

 

Two options were discussed:

  1. Two different syntaxes , same semantics
  2. Abstract syntax into which concrete syntaxes are mapped

The group decided to adopt the abstract syntax approach.

 

Each concrete syntax would share the same character encoding.

 

How do we specify the abstract syntax?

            Mathematical English

            If EBNF is sufficient, we will use that

 

Consensus:

  1. We will define an abstract syntax for Logical Foundations. We will specify concrete syntaxes for KIF, CG, Infix FOL, and an XML-friendly syntax.
  2. Chris Menzel will provide a first draft of the abstract syntax.

 

 

Relationship to Ontology Languages Standards Projects

 

The following people will be liaisons to other standards projects:

 

 

Sorted KIF

Relationships between sorts and the Web ontology languages

 

Mark: Sort names are disjoint from predicate names; we do not want to infer new sort information

 

Options:

  1. Sorts are specified syntactically; there are new logical symbols (e.g. Sort)
  2. Sorts are specified axiomatically using a “Structural Ontology”
  3. Restricted quantifiers

 

Mark: we need sort symbols in the language, but we don’t need a way of specifying the sorts themselves. In the KIF syntax, we have a provision for sort symbols, but the relationship between  sorts is not addressed within the language itself. A sort system is a “plug-in” to KIF.

 

Pat: A sorted language is processed at parse time, without inference; with this criterion, the axiomatic approach does not define a sorted language at all.

 

What inferences can be made in a sorted language that would not be made in an unsorted language?

 

Sorted KIF will provide for:

 

What will be the new logical symbols for sorts?

 

Issues with Sort Declarations:

 

What is a classifier theory?

This may be closer to a “classifier engine” (API) that responds to queries about sorts; we would specify an interface that given a set of sort symbols returns their intersection. This will be a special form of ontology importation. e.g. (sort-theory URI). We could also consider sort theories to be analogous to foreign function calls.

 

What does this mean for a declarative language? I.e. what are the consequences of this importation with respect to model theory?

 

Unresolved Issues:

 

Restricted Quantifiers

Sowa: Can restricted quantifiers faithfully play the role of a sorted language?

 

What is the syntax for restricted quantifiers?

 

Option 1: (forall ((?x :sort dog) (?y :sort cat)) (chases ?x ?y))

Option 2: (forall ((?x dog) (?y cat)) (chases ?x ?y))

Variant 1: (forall ((?x dog) (?y cat) (chases ?x ?y) (?z human)) (owner ?z ?x))

Variant 2: (forall ((dog ?x) (cat ?y)) (chases ?x ?y))

 

Note: Option 2 is satisfied by the BNF of KIF98

 

Example with Boolean combinations of sorts:

(forall (?x (& Sort1 Sort2)) (predicate ?x))

 

Action Items

  1. Sorted KIF will be based upon Pat’s initial proposal for the syntax of sort declarations. He will tidy it up for review by the group.
  2. Adopt KIF98 BNF for restricted quantification.

 

 

Sequence Variables

Should we allow sequence variables in arbitrary position if we don’t have a complete implementation?

 

Consensus:

 

 

Ontology Management Issues

 

Do modules have names, or do we assign names to individual axioms/sentences?

 

What exactly is a module?

 

Any solution to this issue should be reusable in MetaKIF when we name propositions at the metalevel.

 

Unresolved Issues

  1. Is it useful to import only a namespace without any axioms?
  2. How is this related to name clashes for nonlogical symbols? e.g. precedes@pat, precedes@michael
  3. What naming convention do we want to adopt?
  4. Do we want the convention that any reference to a module means that the axioms of the module are automatically imported?
  5. Should we require that all identifiers have URI references? (after discussion, I believe that we thought “no”, but I don’t think that there was explicit consensus on this).

 

 

Requirements

  1. Names for modules and sentences  (this should include a characterization of modules and their relationship to URIs)
  2. Syntax for importing modules

 

 

Action Items

 

Conformance Issues

 

Conformance to KIF is defined with respect to software applications.

A syntactic software application shall be conformant if it is able to parse a set of KIF sentences.

Conformance for inference systems is defined in the draft.

 

The purely syntactic notion of conformance that applies to applications such as parsers, translators, and editors

 

Alternative: Every conforming system must be able to at least parse an arbitrary KIF sentence.

 

Proposed conformance levels for sequence variables

  1. full sequence variables
  2. common restriction (i.e. sequence variables only in tail)
  3. no sequence variables (first-order)

 

Proposed syntactic conformance levels

  1. wild west syntax
  2. no variables in predicate position; function and predicate symbols are disjoint

 

Proposed conformance levels below first-order

Predefine a small set of classes, but allow the extension of this set within MetaCL

Action Items

 

MetaKIF

Requirements:

  1. quote and unquote
    1. specification of the abstract syntax of KIF as a KIF theory, with the constructs in the abstract syntax being elements of the domain
    2. Define an operator that yields terms when applied to formulae. The semantics guarantees that the denotation of a quoted expression is the expression that is quoted; expressions are part of the domain.
  2. sequence-of operator that constructs sequences?
  3. wtr (weak truth predicate)
    1. The current treatment in KIF98 should be adequate

 

We need to be able to quantify into quote (at least to write axiom schemae), but you can’t quantify over an ill-formed expression.

            What would this mean for sequence quantifiers in the metalanguage?

 

Test Cases:

  1. axiom schema for PA and other theories
  2. definition of simple state formula in Reiter’s axiomatization of situation calculus
  3. stratified Horn theory

 

Action Items

 

Other Issues

Do we want to include explicit datatypes in Common Logic?

                                                     i.     In this approach, we are “importing” datatypes rather than explicitly defining them within KIF. The external specification of the datatypes plays the role of the classifier theory.

 

Do we want a string quote operator in the basic language (MetaKIF would contain the structural quote)?

 

Mike Genesereth advocated the inclusion of features to support closed world assumptions and related nonmonotonic reasoning; there was little broad discussion of this topic.

 

Action Item

 

Future Planning

We are renaming the project to be Common Logic

 

Resume monthly telecon schedule (beginning April 23)

 

Chris will create a website for the project on his tamu server.

(add John to kif list as jmclists@cs.stanford.edu)