NEWS: Common Logic

I thought this message from John Sowa would be of interest.
It was posted to the SUO mailing list (see http://suo.ieee.org/
for information and list archives) and describes efforts to
revive efforts to develop an ISO standard for a logic interlingua.

-------- Original Message --------
Subject: SUO: Common Logic Standard
Date: Sat, 06 Apr 2002 11:00:39 -0500
From: "John F. Sowa" <sowa@bestweb.net>
To: standard-upper-ontology@ieee.org, cg@cs.uah.edu

On March 21 and 22, Mike Genesereth hosted a meeting at Stanford
University of the working group on the proposed ISO standards for
the Knowledge Interchange Format (KIF) and Conceptual Graphs (CGs).
The minutes of the meeting are posted at the following URL:

    http://cl.tamu.edu/minutes/stanford-minutes.html

Since the minutes are rather brief, they may be cryptic to those
who did not attend.  I'm writing this note to expand some of the
remarks and their implications.

One of the significant decisions was to choose a new name,
Common Logic (CL), for the proposed standard.  The intent is to
reduce any bias toward the two starting notations, KIF and CGs,
and to emphasize the common basis in first-order logic, as it
was originally developed by Frege, Peirce, Schroder, Peano, and
many others during the late 19th and early 20th centuries.

In keeping with that decision, CL will be defined by an abstract
syntax, which specifies the major categories, such as Quantifier,
Negation, and Conjunction, without specifying any concrete symbols
for writing them.  At the abstract level, even the ordering is
left undefined so that there is no bias toward a prefix notation
such as KIF, an infix notation such as predicate calculus, or a
graph notation such as CGs (or Peirce's original existential graphs).

Since it is impossible to write a purely abstract syntax, the CL
standard will also contain grammars for three concrete syntaxes:
KIF, CGIF (the CG interchange format), and traditional predicate
calculus (TPC) with a Unicode encoding of the commonly used symbols.
Each of those grammars will specify how the abstract categories are
mapped to the printable (or computer representable) symbols of their
notations.  Any of the three concrete notations can be mapped into
any of the others by reversing the mapping from concrete to abstract
in one notation and then mapping from abstract to concrete in the
other notation.

The standard will also contain a version of model theory defined
in terms of the abstract syntax.  The model theory will specify
the truth conditions for any abstract statement, and any conforming
concrete statement in any syntax that is mapped from that abstract
statement would be required to have exactly the same truth conditions.
This requirement will ensure identical semantics for statements
represented in any concrete syntax that conforms to the standard.

Besides the three concrete syntaxes that are currently planned for
the standard, we also discussed plans for an XML-based syntax that
could be mapped directly to the abstract syntax.  For example, the
abstract category Conjunction would be expressed differently in
each of the three concrete syntaxes.  Instead of giving a separate
mapping to XML from each of the concrete syntaxes, it would be
simpler to map the abstract category directly to the XML form
<conjunction>... </conjunction> without specifying which of the
three concrete syntaxes was the original source or the intended
target of the information.

Although the CL project grew out of a collaboration between the
KIF and CG communities, we hope that the CL standard can be used
for many other languages that have a declarative semantics, such
as RDF, UML, DAML, or Topic Maps.  Any language that can be mapped
to and from the CL abstract syntax would automatically inherit the
same model-theoretic semantics and would therefore be semantically
compatible and interoperable with software based on any other
languages that adopt the CL semantics.

Since different languages have different expressive powers, it
might not be possible to map every feature of the abstract syntax
into each of them.  For KIF, CGIF, TPC, and the XML form, every
feature of the abstract syntax will be expressible in the concrete
notations.  Other declarative languages, however, might not have
the same expressive power.  Such languages could only express a
subset of the statements expressible in the abstract syntax.

Several other questions were also discussed and tentative answers
were considered.  Following are the questions, and the most widely
accepted answers.  Further discussion of the implications of the
various options is encouraged.

  Q: How will the CL standard relate to the W3C standards for
     symbols, formats, and naming conventions?

  A: The CL standard will be compatible with all the accepted W3C
     standards.  Following are some of the issues:

      1. There will be an XML representation of the abstract categories,
         which will conform to all accepted W3C standards.  There may
         also be XML representations of the concrete syntaxes as well.

      2. The basic symbol set of both KIF and CGIF does not require
         any symbols beyond the basic 7-bit ASCII, but it will permit
         Unicode character strings and identifiers with conventions
         similar to Java.  TPC notation will require Unicode for the
         special logical symbols, but they could also be represented,
         as in HTML and XML, by symbols like &forall; or &exist;.

      3. The globally unique URIs specified by the W3C could be used
         in any concrete CL syntax.  URIs may have two parts:

             doc-id#frag-id

         where the doc-id identifies a document and the frag-id
         identifies a fragment within the document.  For any concrete
         CL notation (KIF, CGIF, TPC, or XML-CL), the doc-id would
         denote some document that contains a collection of
         statements in that notation; and the frag-id would be
         some identifier defined and used in those statements.  For
         references within a CL document, only the frag-id would be
         used; but global references to other documents would use
         both the doc-id and the frag-id.

  Q: Will CL support unrestricted quantifiers, sorted quantifiers,
     or restricted quantifiers?

  A: Some version of sorted or restricted quantification will be
     supported.  As a result of previous collaboration between the
     KIF and CG communities, the KIF 3.0 document provided a notation
     for restricted quantifiers to represent the type lables in CGs.
     As an example, the following CGIF represents the English sentence
     "A cat is on a mat":

        [Cat: *x] [Mat: *y] (On ?x ?y)

     This graph can be translated to the following statement in
     KIF 3.0 notation:

        (exists ((?x Cat) (?y Mat)) (On ?x ?y))

     In KIF 3.0, Cat and Mat are treated as monadic predicates,
     and the above statement is semantically identical to the
     following version, which uses unrestricted quantifiers:

         (exists (?x ?t) (and (Cat ?x) (Mat ?y) (On ?x ?y))

     However, some implementers, such as Mark Stickel, distinguished
     the sort identifiers from the monadic predicates in order to
     do better syntax checking and to allow improved performance
     during the theorem-proving process.

     The consensus was that some version of sorted or restricted
     quantification will be supported by CL, but no decision was
     made on the question of strict sorting (which would permit
     compile-time checking instead of run-time checking).

  Q: Will CL support contexts?  Will nested contexts be permitted?
     If so, what is the semantics?

  A: CL will provide a mechanism for breaking up a collection of
     statements into contexts, which can be nested arbitrarily deep.
     The CL identifiers will use segmented notation to specify the
     nested levels of contexts.  For example, an identifier, such as
     abc.def.xyz would represent an entity xyz in context def, which
     is nested in context abc.  The identifier "abc.def.xyz" would
     correspond to a frag-id within a CL document.  If preceded by
     a doc-id, it could refer to something in a different CL document.

     No decision was made on the separator between segments.  Another
     suggestion was to use the slash, as in abc/def/xyz. The semantics
     of the contexts is determined by the metalevel facilities of CL.

  Q: What are the metalevel facilities of CL?

  A: The details of the metalevel are still undecided, but various
     participants in the working group have proposals, which they
     will present later.  Following are some of the suggestions:

      1. An important reason for contexts is grouping, so that
         one or more statements or graphs can be identified by
         a frag-id.  Such grouping would be transparent and would
         not affect the semantics -- i.e, multiple statements in a
         context are impliclitly connected by conjunction, whether
         or not they happen to be grouped in various ways.

      2. A group of statements in a context may be the argument of
         a predicate or relation.  The meaning of that context is
         determined by the axioms that define the relation.  Those
         axioms must be in a context outside the context that is
         contained in the argument.

      3. Tarski's hierarchy of metalevels, as he defined it in his
         1933 paper, avoids the usual paradoxes about metalevel
         references.  Some semantics along those lines is being
         considered, but other alternatives may also considered.

      4. The metalevel operations will be able to refer to the
         named contexts and their contents as characterized by the
         abstract syntax.  Since the abstract syntax is independent
         of any concrete syntax, it would be possible for a KIF or
         CGIF statement to refer to the abstract parts of a context
         independently of the concrete syntax that was used to define
         the contents of that context.

For other topics considered, see the minutes.  For any other questions,
please reply to the above email lists for discussion.

John Sowa

Received on Sunday, 7 April 2002 15:07:37 UTC