[SCL] Structure of CGs and predicate calculus

[John F. Sowa]

Michel Chein made the point that there is a
very strong relationship between the structure
of conceptual graphs and predicate calculus
and that the implementation techniques are
almost identical for the two.

Note the word "almost".  I'd like to explain
what that exception implies.  The first point
is that there is an exact isomorphism between
the CG contexts and coreference labels and the
quantifier scopes and variables of predicate
calculus:

   Predicate Calculus         Conceptual Graphs

     Quantifer Scope    <-->       Context

        Quantifier      <-->    Defining Label

      Bound Variable    <-->      Bound Label

Re almost:  The only structural difference between
CGs and predicate calculus is in the ordering of
the items within a context:  the predicates in
predicate calculus are linearly ordered as they
are written from left to right, but the CG concept
and relation nodes are unordered.

This difference is the same as that between a set
and a sequence:  a CG context is the conjunction
of a set of nodes, and the pred. calc. equivalent
is the conjunction of a linear sequence.

The next question what this means.  The exact
isomorphism of the quantifiers and scopes implies
that the context-sensitive rules for variables
and scopes are identical.

The difference in the linear ordering within
a context implies that the rules for the
commutativity of the AND and OR operators
in predicate calculus are irrelevant in CGs.
For example, there must be rules or axioms
to say or imply that the following are
equivalent in predicate calculus:

    (A & B & C)  <-->  (C & B & A)

    (A | B | C)  <-->  (C | B | A)

In CGs, the content of a context is a unordered
set of nodes, so there is no way to make such
a distinction.  In CGIF, it is necessary to say
that the linear ordering of the way the nodes are
listed is irrelevant.

This difference does have an effect on the proof
theory, since the unordered collection of nodes
implies fewer steps in a proof when the ordering
of the nodes in a context can be ignored.

Many implementations of theorem provers simplify
the proofs by taking into account the commutativity
of AND and OR by treating all the nodes within a
context as unordered.  In effect, those theorem
provers are actually designed for conceptual graphs,
and they only use predicate calculus notation for
input and output.  Internally, they are "really"
CG theorem provers.

There are also other aspects of graphs that can
speed up certain kinds of algorithms, but that is
a much more detailed discussion we can save for later.

John Sowa