ISO Common Logic Standard Proposed
Date: Sat, 06 Apr 2002 11:00:39 -0500 From: "John F. Sowa" <firstname.lastname@example.org> To: standard-upper-ontology@IEEE.org, email@example.com Subject: Common Logic Standard
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:
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 ∀ or ∃.
3. The globally unique URIs specified by the W3C could be used in any concrete CL syntax. URIs may have two parts:
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.