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:

• Web ontologies: Pat
• TPTP: Mark (conformance issues are raised here, since it uses “boring FOL”)
• Prolog: Michael Gruninger
• Description logics: Chris Welty
• UML/OCL : ?

 

 

Sorted KIF

Relationships between sorts and the Web ontology languages

• Classes in these languages are the sorts hierarchies in KIF
• Would this go as far as description logics?

 

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:

• Mechanisms for declaring sorts
• Indicating that the language is sorted
• Is this simply a reference to a classifier theory?
• Assigning sort signatures
• Reference to “classifier theories”
• Sorted quantification (will look like restricted quantifiers)

 

What will be the new logical symbols for sorts?

• is-sort, sort-of
•  domain, range?
• operations on sorts

 

Issues with Sort Declarations:

1. How do we assign sort signatures e.g. Boolean products of sorts
2. Proposal for sort signatures: begin with Snark’s treatment
3. Mark: KIF should provide a way of declaring sort signatures, but not sort relationships

 

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?

• the classifier theory is an ontology that restricts the models of a KIF theory
• contradictions in the classifier theory are syntactic errors in the sorted theory
• this would perhaps involve a demonstration that the classifier theory is conformant with KIF

 

Unresolved Issues:

• do we allow empty sorts?
• Overloading sorts
• Are variables, constants, and function symbols sorted?
• Are sort declarations coercive or constraining?

 

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:

• The resolution of this question rests on the approach taken for conformance levels – if we allow partial conformance (i.e. conformance levels), then there is no issue here. If we do not allow such a conformance level, then we must predefine the sublanguage to which all systems must conform.

 

 

Ontology Management Issues

 

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

• Problem: URIs refer to documents, but there may be several  modules within the document.

 

What exactly is a module?

• Do modules have their own URIs?

 

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)
• Minimal requirement: support the capability of importing all sentences in some module
2. Syntax for importing modules

 

 

Action Items

• Request for proposals for the above requirements (to be discussed by email)
• Review Pat’s notes “Namespaces and inclusion”

 

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

• Michael Gruninger will provide a revision of the conformance clauses

 

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

• Chris Menzel will provide a first draft of the semantics for quote/unquote

 

Other Issues

Do we want to include explicit datatypes in Common Logic?

• e.g. strings, numbers, XML Schema datatypes
• Can we simply provide guidance for translators from a language with datatypes (e.g. XML) such that datatypes are mapped to sorts within KIF?

                                                     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

• Pat will provide a strawman proposal for datatyping

 

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)