[SCL] Common Logic and CGs
John F. Sowa
sowa at bestweb.net
Wed Apr 9 12:27:31 CDT 2003
Yesterday, there was a teleconference with some of
the people who are developing the Common Logic
standard. At the end of this note is a message
from Pat Hayes, which summarizes the discussion.
I'd like to expand some of the points and their
implications for conceptual graphs, KIF, and
other notations for logic. For more info about
Common Logic, see the web site (which includes
pointers to slides that Chris Menzel and I
presented in January):
http://philebus.tamu.edu/cl/
Following are some of the basic issues:
1. The Common Logic core is untyped, and it makes
no distinction between individual entities and
predicates (or relations). That means it is
possible to use variables to refer to predicates
and to quantify over them in the same way as
any other entity.
2. The ability to quantify over predicates has the
effect of a higher-order logic, for many purposes,
but the fundamental CL model theory is purely
first-order. That might sound paradoxical, but
the basic point can be explained by noticing
that it is possible to have a logic with just
one relation named "apply". Then instead of
a predicate P(x), you would write apply(P,x),
which means that the entity named P is applied
to the entity named x.
3. But for the model theory, an individual entity
represented by x and a predicate represented
by P are not distinguished syntactically.
However, most notations do make a distinction
between predicates (or relations) and individual
entities. Therefore, there will be a predicate
to distinguish them. For the example mentioned
in point #2, relation(P) would be true, but
relation(x) would be false. In a notation that
makes a syntactic distinction between relations
and individual entities, the syntax P(x) would be
logically equivalent to the following expression:
P(x) & relation(P) & ~relation(x)
4. Since the CL core and model theory are unusual,
they raise many questions, and they could lead
to possible misunderstandings. Therefore, the
CL documentation will present the material in
a systematic way that will emphasize the support
for classical first-order logic and the various
extensions, such as conceptual graphs and KIF.
Since CL is defined by an abstract syntax, some
concrete notation is needed for examples. To
avoid presenting every example in every notation,
the primary concrete notation will the the
traditional predicate calculus notation, with
the usual symbols such as upside-down A and
backward E. There will also be some examples
that show the equivalents in CGs, KIF, OWL,
RDF, etc. People who are only interested in
one or another of those languages would not
use the CL documentatation, but the more
specific documentation for their pet notation.
5.
-------- Original Message --------
Subject: [SCL] minutes of telecon 8 April 03
Date: Tue, 8 Apr 2003 16:03:32 -0400
From: pat hayes <phayes at ai.uwf.edu>
Reply-To: scl at philebus.tamu.edu
To: scl at philebus.tamu.edu
Present: Herman ter Horst, Tamel Tamet, John Sowa, Pat Hayes, Chris Menzel.
1. Presentation of material.
(Issue raised by Tamel). Tamel has suggested that the material be
presented as a 'standard' FO syntax initially and primary, with both
restrictions and extensions described as optional. Pat suggested a
compromise, but the group agreed with Tamel that the pedagogic
advantages of this approach outweighed any considerations of
elegance. John suggested that many readers will not read the MT in
any case and it should be late in the document. Chris suggested that
some place in the document should present the unified family of
languages so as to demonstrate the unity.
There was broad agreement (possible exceptions indicated by ?) on the
following overall structure, more or less:
- Introduction providing broad summary and motivation.
- Abstract syntax of the conventional FO fragment as a 'core'.
- Concrete syntaxes related to the abstract syntax. (One of them, as
conventional as possible,to be chosen as the syntax to present
examples in the text.)
- Extensions to the core
- comment wrappers [could be part of the core?]
- externally defined namespaces [do we want to build any into the
core, eg numerals, strings?]
- freer syntax allowing quantification over relations
- variadic relations and row variables
- Restrictions to (extensions to) the core.
- Unified summary of language hierarchy
- Model theory stated generally
- how MT for core connects to conventional MT.
- Discussion of relationships between levels, eg 'holds', and how row
variables can or cannot be mapped using lists?. Also examples of
valid reasoning patterns of general utility, including the use of
induction-style reasoning on recursive row-variable definitions.
-------
2. Core language. We agreed that the core should allow restricted
quantification as useful syntactic sugar, but should not attempt to
include types or more advanced concepts.
One issue we did NOT discuss, by the way, is whether the core should
allow function symbols and full terms (I vote yes), and whether or
not it should restrict relations and functions to have a fixed arity
(I vote no*); and if so or not, whether or not a user can assert that
a given relation or function has a certain arity. Certainly in the
full syntax, arity could presumably be a property of a relation , and
perhaps we should provide a logically defined syntax for asserting
those properties. Comments?
(* To clarify: not including an arity constraint into the syntax,
that is: it would be too much trouble to take it out again for the
generalized syntax, and I don't think it is really necessary even for
conventional FO syntax. In the conventional language, two uses of the
same symbol with different arities are essentially treated
semantically and in proofs as different symbols, and does no harm.)
-------
3. Built-in logical names and externally defined namespaces
The core should include equality.
The full syntax should include an 'is-a-Relation' predicate.
(and Arity predicates?)
Special name domains should provide a built-in logical predicate true
of entities in the domain, so that an atom formed by applying that
predicate symbol to any special name with the appropriate syntax will
be true.
We need a way to specify the syntax of names in a special-name
domain. We did not reach agreement on how to do that. Here are some
options:
1. Do not provide one, but instead restrict ourselves to a small set
of built-in special name categories, eg numerals and quoted character
strings, or maybe a set based on the XML schema built-in datatype
domains. This would be quick and dirty but might be worth doing even
as an exercise for ourselves :-)
2. Simply require that whoever defines 'an SCL language' provide a
BNF for their particular syntax of special names, and write their own
parsers.
In my view, neither of these is really adequate. The second option
basically makes it impossible to write a general SCL parser, since
particular SCL languages may have arbitrary syntactic complexities
which might need to be parsed, and the reversion to BNF allows too
low-level and detailed a possible relationship between special name
syntax and the rest of the language. I would be happier if we could
provide a more coherent mechanism which defines the syntactic
interface between special name domains and the rest of the language
more clearly. However I confess I have no clear idea of how to do
that in an appropriate way.
-----
If I have forgotten anything or got anything wrong, please send
corrections to the list. And any other points arise, of course. And
any comments on the [...?] questions noted above gratefully received.
Actions:
Pat to complete draft of initial document (continued)
John to write sketch of CG generalized concrete syntax
Chris to adapt CL abstract syntax to the SCL core case
Next telecon at same time on the 22nd. I will send a reminder a few
days ahead hopefully with something resembling an agenda. (BTW, the
telecons get more productive when we have more details to deal with,
to make y'all feel somewhat more optimism.)
Pat
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32501 (850)291 0667 cell
phayes at ai.uwf.edu http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu for spam
_______________________________________________
SCL mailing list
SCL at philebus.tamu.edu
http://philebus.tamu.edu/mailman/listinfo/scl
More information about the Scl
mailing list