SUO: Re: Common Logic Standard
Bill,
Although I have many times emphasized the equivalent expressive
power of the KIF and CG standards, I have also emphasized the major
differences between the algebraic notation and the graphic notation
for computational and heuristic purposes as well as pedagogy.
If I haven't emphasized those reasons in some of our discussions,
it is only because we were too busy discussing many other topics.
> JA, you are simply mistaken if you think that syntax has any impact
> on the ability of ATP systems to solve problems. I can't think of
> any real ATP system that pays any attention to the input syntax once
> the parse of the problem set is done with.
This statement leads to the heart of the disagreement. Although I
agree with Bill that after the external syntax has been parsed
it can be mapped into any internal form that is suitable for the
available algorithms, the differences in the external form have a
strong influence on what internal forms the programmer chooses, and
therefore, on the choice of algorithms.
Remember that all the best mathematicians and programmers are lazy
-- that is their greatest virtue, but sometimes their greatest vice.
They always look for the shortest and simplest way to represent any
problem. In many cases, that simple way is indeed the best. But
for many other cases, what is simple to program in one language
may turn out to be extremely difficult and complex in another.
For better or worse, one of the reasons why AI people find the KIF
syntax attractive is that it is automatically parsed by the LISP
input reader (and it is not difficult to parse in most languages
other than COBOL). Then the simplest internal representation
of the parsed result is a tree (with occasional cross links to
represent more complex graphs).
For many algorithms, trees are excellent representations. For theorem
provers, a rooted tree is much easier to unify with another rooted
tree than to unify two arbitrary graphs. That is one reason why
the search for good algorithms for doing CG theorem proving caused
many implementers to translate the CGs to some other notation and
use conventional theorem provers.
However, Bob Levinson made major breakthroughs in graph-based
algorithms because he started with graphs that represented organic
molecules. Those graphs tend to get very large, and they have no
natural roots, but they often have important symmetries that can be
exploited. Bob has been working on exploiting those symmetries
for nearly 20 years, and he has found algorithms, which for certain
kinds of problems, attain efficiencies that go far beyond what has
been done in the theorem provers written by programmers who think
in algebraic terms. Gerard Ellis spent a year working with Bob,
and the two of them developed techniques that are, in fashionable
terminology, "significantly beyond the state of the art". Another
programmer who started with CGs, Arun Majumdar, discovered other
graph-based algorithms for finding analogies that Marvin Minsky
and his crew at MIT couldn't believe would work -- but they do.
I certainly agree that those graph-based algorithms could be applied
to information represented in the algebraic notation. That is why
I participate in the Common Logic standards project. I want to take
all that data lying around that has not be exploited with the old
technology and run it through the graph-based technology.
For a discssion of the heuristic power of graphs, which enabled Peirce
to discover a more general and powerful form of natural deduction 37
years before Gerhard Gentzen, see my annotated version of MS 514:
http://www.jfsowa.com/peirce/ms514.htm
For a brief summary of the advantages of graphs over the old-fashioned
technology, see my paper "Architectures for Intelligent Systems":
http://www.jfsowa.com/pubs/arch.htm
Sections 2 and 3 talk about human factors, but Sections 3 and 4 get
into the issues of graph algorithms and computability. I admit that
those same algorithms could be used with an external syntax in an
algebraic form, but they were only discovered by people who thought
directly in terms of graphs. For a discussion of how important
those algorithms are to practical problems (i.e., they can save
a company several millions of dollars), see the example at the end
of my slides for the KT 2002 Conference:
http://www.jfsowa.com/talks/negotiat.htm
John Sowa