Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

NY Times (10 Dec) report on Larry Wos's achievement

399 views
Skip to first unread message

MCKAY john

unread,
Dec 10, 1996, 3:00:00 AM12/10/96
to

Gina Kolata reports effervescently on a computer proof
of some equational definition of a boolean algebra.
Please will someone fill in the mathematical details?

JM

--
Deep ideas are simple.
Odd groups are even.
Even simples are not;
and Gal/F2(t)(x^24-x-t) = Mathieu group, M24.

Matthew P Wiener

unread,
Dec 11, 1996, 3:00:00 AM12/11/96
to

In article <58krc3$l...@newsflash.concordia.ca>, mckay@cs (MCKAY john) writes:
>Gina Kolata reports effervescently on a computer proof of some
>equational definition of a boolean algebra. Please will someone fill
>in the mathematical details?

I have no idea, but my impression was the the article was ridiculously
overblown. The equality of two equational varieties is of course an
ideal computational problem.

For example, Ken Kunen has two recent papers in JOURNAL OF ALGEBRA,
where he works out which Moufang identities imply each other. The
papers are mostly a summary of the computer calculations.

Why the one gets into the NYT as major news and the other one doesn't
makes absolutely no sense to me. Is there something nontrivial going
on?
--
-Matthew P Wiener (wee...@sagi.wistar.upenn.edu)

Norman D. Megill

unread,
Dec 11, 1996, 3:00:00 AM12/11/96
to

In article <58krc3$l...@newsflash.concordia.ca>,

MCKAY john <mc...@cs.concordia.ca> wrote:
>Gina Kolata reports effervescently on a computer proof
>of some equational definition of a boolean algebra.
>Please will someone fill in the mathematical details?

The following information is from the Robbins algebra home page
(sorry, I lost the url but you can probably find it with AltaVista)

Also, the problem is discussed in
\bibitem{Wos} Wos, Larry, Ross Overbeek, Ewing Lusk and Jim Boyle, {\em
Automated Reasoning: Introduction and Applications}, second edition,
McGraw-Hill, Inc., New York, 1992.

From the web page:

In 1933, E. V. Huntington presented the following basis for
Boolean algebra:

x + y = y + x. [commutativity]
(x + y) + z = x + (y + z). [associativity]
n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation]

At that time, Herbert Robbins, a student of Huntington, conjectured
that the Huntington equation can be replaced with a simpler one [5]:

n(n(x + y) + n(x + n(y))) = x. [Robbins equation]

Robbins and Huntington could not find a proof, and the problem was
later studied by Tarski and his students.

Algebras satisfying commutativity, associativity, and the Robbins
equation became known as Robbins algebras. It is clear that every
Boolean algebra is a Robbins algebra, so the interesting problem was
whether every Robbins algebra is Boolean.

-Norm Megill

Herman Rubin

unread,
Dec 11, 1996, 3:00:00 AM12/11/96
to

In article <58mdvl$o...@netnews.upenn.edu>,

Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:
>In article <58krc3$l...@newsflash.concordia.ca>, mckay@cs (MCKAY john) writes:
>>Gina Kolata reports effervescently on a computer proof of some
>>equational definition of a boolean algebra. Please will someone fill
>>in the mathematical details?

>I have no idea, but my impression was the the article was ridiculously


>overblown. The equality of two equational varieties is of course an
>ideal computational problem.

I agree. And they could not even get Tarski's first name and the
university where he taught correct.

>For example, Ken Kunen has two recent papers in JOURNAL OF ALGEBRA,
>where he works out which Moufang identities imply each other. The
>papers are mostly a summary of the computer calculations.

>Why the one gets into the NYT as major news and the other one doesn't
>makes absolutely no sense to me. Is there something nontrivial going
>on?

It was pointed out that computers have found "trivial" proofs before,
by search.

It is CLAIMED that the computer was doing more than verification.
I am far from convinced that anything programmed can do so.
--
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Dept. of Statistics, Purdue Univ., West Lafayette IN47907-1399
hru...@stat.purdue.edu Phone: (317)494-6054 FAX: (317)494-0558

Tal Kubo

unread,
Dec 11, 1996, 3:00:00 AM12/11/96
to

Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:
>In article <58krc3$l...@newsflash.concordia.ca>, mckay@cs (MCKAY john) writes:
>>Gina Kolata reports effervescently on a computer proof of some
>>equational definition of a boolean algebra. Please will someone fill
>>in the mathematical details?

See http://www.mcs.anl.gov/home/mccune/ar/robbins.

>
>I have no idea, but my impression was the the article was
>ridiculously overblown.

Second that impression.


>The equality of two equational varieties is of course an
>ideal computational problem.
>

>For example, Ken Kunen has two recent papers in JOURNAL OF ALGEBRA,
>where he works out which Moufang identities imply each other. The
>papers are mostly a summary of the computer calculations.

According to Kunen, those papers were intended to advertise to
mathematicians the potential of automated reasoning. He used some
of the same software described in the NYT article.

"...in order to really establish the usefulness of these methods, we
need to get the mathematical results of automated reasoning published
as standard mathematics in standard mathematics journals, refereed by
standard mathematicians who have no particular interest in promoting
automated reasoning". (http://www.cs.duke.edu/NSFwkshopAD/wkshop/kunen.html)


>
>Why the one gets into the NYT as major news and the other one doesn't
>makes absolutely no sense to me. Is there something nontrivial going
>on?

J. AlGEBRA doesn't provide tip sheets or press releases to the papers.
Maybe the AI journals are better at generating hype...


David K. Davis

unread,
Dec 12, 1996, 3:00:00 AM12/12/96
to

MCKAY john (mc...@cs.concordia.ca) wrote:
: Gina Kolata reports effervescently on a computer proof
: of some equational definition of a boolean algebra.
: Please will someone fill in the mathematical details?

Just a comment: several years ago I spent a lot of time using Prolog, a
computer language that implements a fragment of the predicate calculus, to
solve Martin Gardner type puzzles - some of them. I say some because the
only cases it (and I) could handle was where the search space could be
kept within bounds. In other cases I either had no idea as to how to set
up the search space, or no idea how to keep it narrow enough that the
search tree could be traversed in my lifetime.

It was great fun. Theoretically, any given piece of mathematics can
axiomatized and some theorem prover can be set to searching to see if an
hypothesis has a proof. But I think it's rare that one can keep the search
narrow enough and bounded in depth enough to deal with something of real
interest. In this case, there was success, and I'm sure that's an
accomplishment. But in no way does this have anything to do with
"intelligence" in any meaningful sense of the word. A computer is close to
beating Kasparov at chess. By doing millions of calculations (tree
searching mostly) a computer can beat the human mind - which is definitely
not doing a brute force tree search. I read somewhere that computers
have to improve a lot to even be hopeless at bridge. In one sense,
mathematics is more like chess, because there is full information. But in
most cases, the search tree widens even more rapidly than in bridge (I
believe).

AI is like old-time religion with its revival meetings and the like.

-Dave D.


Gene W. Smith

unread,
Dec 12, 1996, 3:00:00 AM12/12/96
to

In article <58mdvl$o...@netnews.upenn.edu>,

Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:

>For example, Ken Kunen has two recent papers in JOURNAL OF ALGEBRA,
>where he works out which Moufang identities imply each other. The
>papers are mostly a summary of the computer calculations.

>Why the one gets into the NYT as major news and the other one doesn't


>makes absolutely no sense to me. Is there something nontrivial going
>on?

The one in the Times would have been an automatic A in Ralph
McKenzie's universal algebra course.


Michael L. Siemon

unread,
Dec 13, 1996, 3:00:00 AM12/13/96
to

In article <58qlkj$q...@river.gwi.net>, gws...@river.gwi.net (Gene W.
Smith) wrote:

+>Why the one gets into the NYT as major news and the other one doesn't
+>makes absolutely no sense to me. Is there something nontrivial going
+>on?

+The one in the Times would have been an automatic A in Ralph
+McKenzie's universal algebra course.

I am tempted to repeat Matthew's question...
--
Michael L. Siemon m...@panix.com

"sempiternal, though sodden towards sundown."

Matthew P Wiener

unread,
Dec 13, 1996, 3:00:00 AM12/13/96
to

In article <mls-131296...@mls.dialup.access.net>, mls@panix (Michael L. Siemon) writes:
>In article <58qlkj$q...@river.gwi.net>, gws...@river.gwi.net (Gene W.
>Smith) wrote:

>+>Why the one gets into the NYT as major news and the other one doesn't
>+>makes absolutely no sense to me. Is there something nontrivial going
>+>on?

>+The one in the Times would have been an automatic A in Ralph
>+McKenzie's universal algebra course.

>I am tempted to repeat Matthew's question...

What's really bizarre about the article is that the landmark being
touted in the NYT article, of a computer being used to "discover" a
proof instead of working out a computation for us, was achieved over
20 years ago, with Appel-Haken's presumed proof of the four color
map theorem. (The notorious A-H difficulties are almost certainly
restricted to the human aspect.)

Not only did their proof include computer verification that each of
their configurations was reducible, the set of configurations was
originally *found* by computer search, and involved replacing near
misses, so to speak, with more likely candidates. This was how
A&H ensured that their final set was unavoidable, and in particular,
the successful branch of their search tree is an essential part of
their final proof.

Michael L. Siemon

unread,
Dec 13, 1996, 3:00:00 AM12/13/96
to

In article <58rtvk$u...@netnews.upenn.edu>, wee...@sagi.wistar.upenn.edu
(Matthew P Wiener) wrote:

+In article <mls-131296...@mls.dialup.access.net>, mls@panix
(Michael L. Siemon) writes:
+>In article <58qlkj$q...@river.gwi.net>, gws...@river.gwi.net (Gene W.
+>Smith) wrote:
+
+>+>Why the one gets into the NYT as major news and the other one doesn't
+>+>makes absolutely no sense to me. Is there something nontrivial going
+>+>on?
+
+>+The one in the Times would have been an automatic A in Ralph
+>+McKenzie's universal algebra course.
+
+>I am tempted to repeat Matthew's question...
+
+What's really bizarre about the article is that the landmark being
+touted in the NYT article, of a computer being used to "discover" a
+proof instead of working out a computation for us, was achieved over
+20 years ago, with Appel-Haken's presumed proof of the four color
+map theorem. (The notorious A-H difficulties are almost certainly
+restricted to the human aspect.)

Yep; and with respect to the intial point I took from your question,
I rather understand (having only read the Times article) that what
grabbed people about this particular proof was its having a history
of (unresolved) attention by some big names, like Tarski. But if, in
fact, the question is ideal for a calculation based approach, one (IMHO)
should *not* regard a failure of human attempts to resolve the conjecture
as being particularly good evidence of its inherent difficulty.

I *do* however, like the notion presented in the Times article, that the
program was able to improve on its first proof. THAT strikes me as very
interesting.

ca314159

unread,
Dec 14, 1996, 3:00:00 AM12/14/96
to

MCKAY john wrote:
>
> Gina Kolata reports effervescently on a computer proof
> of some equational definition of a boolean algebra.
> Please will someone fill in the mathematical details?
>
> JM
>
> --
> Deep ideas are simple.
> Odd groups are even.
> Even simples are not;
> and Gal/F2(t)(x^24-x-t) = Mathieu group, M24.


Mccune's page and the source code

http://www.mcs.anl.gov/home/mccune/ar/robbins/


--
http://search.dejanews.com/dnquery.xp?query=ca314159&defaultOp=AND&svcclass=dncurrent&maxhits=100&showsort=date&site=yahoo

Alex Lopez-Ortiz

unread,
Dec 15, 1996, 3:00:00 AM12/15/96
to

In article <58rtvk$u...@netnews.upenn.edu>,

Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:
>
>What's really bizarre about the article is that the landmark being
>touted in the NYT article, of a computer being used to "discover" a
>proof instead of working out a computation for us, was achieved over
>20 years ago, with Appel-Haken's presumed proof of the four color
>map theorem. (The notorious A-H difficulties are almost certainly
>restricted to the human aspect.)

I disagree. In the four-colour theorem case, most of the proof work
was done by humans (effectively noticing the reducibility to basic
forms and selecting them), and it was only the few last steps that
were finished by the computer.

In this case, from what the NYT article says, the work done by the humans
was of a general nature (improving the authomatic prover) and the computer
did all the rest, on a "certifiable hard" problem.

The two problems that Matthew has mentioned are not equally relevant.
The previous article solving a similar question did not involve a
"certifiable hard problem", the four colour theorem is a computer
assisted proof.

Me? I was happy to see math and computers (two of my life passions)
so prominently displayed on the NYT, for the laymen to share on
them.

Alex
"keeper of the FAQ"

--
Alex Lopez-Ortiz alop...@daisy.UWaterloo.ca
http://daisy.uwaterloo.ca/~alopez-o Research Scientist
Open Text Corp. 185 Columbia St W Waterloo, Ont N2L 3L3 Canada

Matthew P Wiener

unread,
Dec 15, 1996, 3:00:00 AM12/15/96
to

In article <E2FM2...@undergrad.math.uwaterloo.ca>, alopez-o@daisy (Alex Lopez-Ortiz) writes:
>In article <58rtvk$u...@netnews.upenn.edu>,
>Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:

>>What's really bizarre about the article is that the landmark being
>>touted in the NYT article, of a computer being used to "discover" a
>>proof instead of working out a computation for us, was achieved over
>>20 years ago, with Appel-Haken's presumed proof of the four color
>>map theorem. (The notorious A-H difficulties are almost certainly
>>restricted to the human aspect.)

>I disagree. In the four-colour theorem case, most of the proof work
>was done by humans (effectively noticing the reducibility to basic
>forms and selecting them), and it was only the few last steps that
>were finished by the computer.

No. Finding the working set was done by a computer search. Some of
the backtracking may have been done by hand--simply because it was
easier at that point than to write one more program.

Figuring out the overall algorithm was of course done by humans.

>In this case, from what the NYT article says, the work done by the humans
>was of a general nature (improving the authomatic prover) and the computer
>did all the rest, on a "certifiable hard" problem.

The difference here is that there are very few questions regarding
reducibility that anyone is interested in, but endless numbers of
questions regarding equational varieties that people study.

Because of that, the A-H software was customized to the particular
question at hand and left at that, nor was it made to put every last
step on automatic. In contrast, software that lets one speed one's
way through your favorite algebraic or deductive systems is quite
often made as general purpose as possible.

>Me? I was happy to see math and computers (two of my life passions)
>so prominently displayed on the NYT, for the laymen to share on them.

I also thought it nice for Robbins to get some positive attention, what
with the second screwing he's gotten regarding his book, this time from
Oxford.

Christopher J. Henrich

unread,
Dec 15, 1996, 3:00:00 AM12/15/96
to

In article <59186n$a...@netnews.upenn.edu>, wee...@sagi.wistar.upenn.edu
(Matthew P Wiener) wrote:


>
> I also thought it nice for Robbins to get some positive attention, what
> with the second screwing he's gotten regarding his book, this time from
> Oxford.
> --
> -Matthew P Wiener (wee...@sagi.wistar.upenn.edu)

I know and love his book, and I saw that a new edition, with Ian Stewart's
name added to the authors, has appeared. Please clarify the circumstances of
Robbins's being "screwed" regarding it.

--
Christopher J. Henrich
chen...@monmouth.com

Herman Rubin

unread,
Dec 15, 1996, 3:00:00 AM12/15/96
to

In article <E2FM2...@undergrad.math.uwaterloo.ca>,

Alex Lopez-Ortiz <alop...@daisy.uwaterloo.ca> wrote:
>In article <58rtvk$u...@netnews.upenn.edu>,
>Matthew P Wiener <wee...@sagi.wistar.upenn.edu> wrote:

>>What's really bizarre about the article is that the landmark being
>>touted in the NYT article, of a computer being used to "discover" a
>>proof instead of working out a computation for us, was achieved over
>>20 years ago, with Appel-Haken's presumed proof of the four color
>>map theorem. (The notorious A-H difficulties are almost certainly
>>restricted to the human aspect.)

>I disagree. In the four-colour theorem case, most of the proof work
>was done by humans (effectively noticing the reducibility to basic
>forms and selecting them), and it was only the few last steps that
>were finished by the computer.

It is true that much of the work in the Appel-Haken proof, including the
varification that all the cases was covered, was done by humans.

>In this case, from what the NYT article says, the work done by the humans
>was of a general nature (improving the authomatic prover) and the computer
>did all the rest, on a "certifiable hard" problem.

Applying an algorithm, no matter how complicated, is not "creative".
The credit goes to the algorithm designers.

Matthew P Wiener

unread,
Dec 16, 1996, 3:00:00 AM12/16/96
to

In article <chenrich-151...@ppp69.monmouth.com>, chenrich@monmouth (Christopher J. Henrich) writes:
>In article <59186n$a...@netnews.upenn.edu>, wee...@sagi.wistar.upenn.edu
>(Matthew P Wiener) wrote:

>> I also thought it nice for Robbins to get some positive attention, what
>> with the second screwing he's gotten regarding his book, this time from
>> Oxford.

>I know and love his book, and I saw that a new edition, with Ian Stewart's


>name added to the authors, has appeared. Please clarify the circumstances
>of Robbins's being "screwed" regarding it.

The first screwing was by Courant. Robbins was just a grad student at
the time, and when the book was finished, Courant put himself down as
sole author with Robbins in the acknowledgements. Robbins saw a proof
in time, and found some important people who put pressure on Courant to
put Robbins down as co-author. Courant did so on the title page and
front cover, but not on the copyright notice.

In those days, copyright was interpreted quite literally, so Robbins was
essentially shut out.

On the other hand, Courant did forward some of the royalties over to
Robbins. Whether it was a fair amount or a smidging fraction of Courant's
share is something that nobody knows.

I get the impression that Courant's heirs did not forward any royalties,
though. They eventually sold the copyright to Oxford, at which point for
sure Robbins never saw another penny.

Over the years, Robbins has made thousands of notes on the book, from
trivial errata to tiny fixes to small rewrites, hoping of course that
some day these could be incorporated. Hence, the second screwing, to
wit, Oxford never asked Robbins, and in fact had Stewart revise the book
for the second edition without ever informing Robbins of anything, so
all this work is pretty much lost now.

Mostly all Stewart did was add an appendix. Big whoop. He did a little
bit of rewriting, but nothing of the sort that Robbins intended. Of
particular interest is Robbins' claim that one of Stewart's rewrites is
actually a subtle error, regarding which see Robbins' forthcoming AMM
article.

David Eppstein

unread,
Dec 16, 1996, 3:00:00 AM12/16/96
to

hru...@b.stat.purdue.edu (Herman Rubin) writes:
> Applying an algorithm, no matter how complicated, is not "creative".
> The credit goes to the algorithm designers.

The tone of your statement above is sounding uncomfortably close to
proof-by-definition. It sounds like you think computers can not be
creative merely because they're computers.

Perhaps you should define your terms more explicitly. What do you mean
by "creative"? And what do you think is special about humans, that
allows them to be creative while denying the same ability to computers?

(Hoping you're not falling into Penrose's quantum voodoo or other forms
of mystical dualist wishful-thinking anthropocentrism...)
--
David Eppstein UC Irvine Dept. of Information & Computer Science
epps...@ics.uci.edu http://www.ics.uci.edu/~eppstein/

Bill Dubuque

unread,
Dec 16, 1996, 3:00:00 AM12/16/96
to mc...@cs.concordia.ca, wee...@sagi.wistar.upenn.edu, gws...@river.gwi.net, alop...@daisy.uwaterloo.ca, hru...@b.stat.purdue.edu

The following old post of mine on brute-force vs. intuition is relevant.
Nothing new needs to be said -- even in light of the recent automated
proof of Robbins conjecture.

The Beauty of Chess is Skin Deep
but the Beauty of Math is Infinitely Deep

Summary: some thoughts on intuition vs. brute-force in chess and math,
motivated by recent discussion of intelligence in chess in the newsgroup
comp.ai.philosophy (after the ACM Challenge: Deep Blue vs. Kasparov).

>From: Drew McDermott <mcde...@cs.yale.edu>
>Newsgroups: comp.ai.philosophy
>Subject: Deep Blue and Intelligence
>Date: Mon, 19 Feb 1996 12:37:20 -0500
>
>The New York Times ran a post-mortem of the Deep-Blue-Kasparov chess
>match today, quoting various notables (Simon, Searle, Hofstadter,
>Gelernter, and others) on the question of whether the machine was
>"really" intelligent. Simon said it was, but the consensus among most
>of the others was that Deep Blue's relative success merely indicated
>that chess, contrary to expectation, requires no intelligence. ...

I conjecture that optimal chess play is essentially random and
of complexity far transcending human comprehension. I base this
conjecture on recent detailed analyses of endgame strategies made
possible via the construction of gigabytes of endgame databases.
These databases supply exact game-theoretic values (win/loss/draw)
and optimal move sequences for small-men endgames (e.g. Ken
Thompson distributes CD's for five-men endgames). Such perfect
information has motivated a reanalysis of the classical
human-derived endgame strategies with a surprising result that
optimal play often violates human heuristics and further may be
so complex in general that it is beyond the grasp of mere mortals.
Grandmasters have had severe difficulties playing against these
endgame databases. Optimal play is so complex that in one case
a recognized endgame expert (Roycroft) was able to comprehend a
certain endgame database only with enormous effort and the aid
of automated inductive-learning algorithms [Her] [Kop] [Mic].
See the Appendix below for an example of such complexity.
If the endgame holds such complexity then human comprehension of
optimal middlegame (and entire game) strategy is surely hopeless.

Such results seem to indicate that chess is random from a resource-
based Kolmogorov complexity point of view; i.e. probably it is not
possible to abstract from optimal play some structured general
strategy because deep tactics may produce exceptions to all human
comprehensible plans and strategies -- a huge endgame database itself
may be the shortest possible description of the optimal strategy.

If this turns out to be true, then human strategies will only be
useful against humans -- deeper searching programs will be able to
refute shallow human strategies. I think that we have already
begun to see some of this in the recent ACM match between
Kasparov and Deep Brute. In the long run it may prove impossible
for humans to comprehend the deep random variations that chess
programs compute as optimal. There may be no flowing themes, just
random forced tactical considerations that stem from deep
searches -- perhaps the beauty of human chess lies only skin deep.

It is important to keep in mind that such brute-force game tree
searching fails miserably once one turns attention to games with
bushier trees, e.g. the game of Go (cf. [Nie] for an excellent
survey on exhaustive search). Human ingenuity still reigns supreme
navigating bushlands in these combinatorially exploding jungles

The same holds true of brute-force tree searching in many other
domains, e.g. theorem proving in mathematics. For example,
recently there has been a flurry of research applying effective
techniques in algebra towards proving elementary theorems in
geometry [Kap]. Thus we now know algorithms that automatically
decide the truth of theorems in elementary Euclidean geometry of
the sort one encounters in high-school, e.g. Appolonius' Circle
Theorem (cf. Appendix below). Such proofs proceed by brute force
calculation instead of geometric intuition, lemmas, analogies,
and all the other techniques that are the common arsenal of the
geometer. Do such algorithms herald the death of geometry? Of
course not, for such algorithms provide absolutely no insight
whatsoever into the structure of a proof -- they churn and grind
and leave us with a solitary bit of truth just as the chess
endgame database leaves us with a win/lose/draw result but no hint
whatsoever of any plan or strategy. But the importance of a proof
or chess game lies much deeper than its result: it may herald the
discovery of a new idea with widespread application or it might
be a prototypical illustration of a general theme, etc -- the
possible utilities are endless. The importance of Wiles proof of
Fermat's Last Theorem stems not from its truth value but rather
from the application of its methods to the Taniyama-Weil
conjecture and its consequent role in the Langlands program --
a major research theme in contemporary mathematics. On the other
hand, the brute-force proof of the four-color theorem contributes
merely a single bit of information to mathematical knowledge.

As another mathematical example I mention a theorem of Jacobson:
a ring is commutative if for every element x there is an integer
n > 1 such that x^n = x. Although this theorem may be proved
automatically for small n by existing brute-force equational
completion-based theorem provers, the general case is thought to
be far out of reach [BL,KZ]. Jacobson's marvelous proof is an easy
corollary of his deep structure theory for rings, a structure
theory which is a prime example of the modern axiomatic method
and structuralistic trend in twentieth-century mathematics. Such
deep and beautiful triumphs of human ingenuity will never be the
result of pure brute-force, no matter how Deep the Brute. The
beauty of chess may lie only skin deep but the beauty of math
transcends even transfinite mechanical depths (as we know from
the deep work of Goedel, Turing, and Feferman [Fe1] [Fe2] [Fe3]).
Long live ingenuity!

-Bill Dubuque

Appendix

"With the relatively small queen-versus-rook ending it is not impossible
that a human could eventually understand, explain and perhaps even
master for his own use the bizarre intricacies of machine play. But
only a small step up the ladder of complexity, to queen and pawn (on
g7) versus queen, is sufficient to exceed such a possibility.
Komissarchik and Futer [1974] built an exhaustive database for this
ending. A computed minimax-optimal strategy takes the white king on a
labored and mysterious journey, circumnavigating the board more than
once, before the preconditions for safe pawn promotion are finally
established. Figure 15.3 from Komissarchik and Futer [KF] 1974 is
reproduced below. Roycroft comments on "... the white king's contorted
peregrinations throughout the solutions full length". Qualified
students of this result believe that human insight into the detailed
rationale is unlikely to be attainable [Roy] 1986."

--excerpted from [Mic], p. 247

Figure 15.3: A king's labored and mysterious journey.

+-----------------------------------------------------------------------+
| | | | | | | | |
| | ------- | | | | -----------+ |
| | / | \ | |\ | | | \ | | |
| | / | \ | | \| | | \ | | |
|--------/--------+--------\----|---+\-------+--------+--------\-----|--|
| / | | | \ | | \ | | | \ | |
| / | | | \| | | | | WP | / | |
| \ | | | | | | |\ | / | |
| \ | | | | \ | | \| / | | |
|--------\--------+--------+--------+-----\--+----|---+\---/---+-----|--|
| | \ | | -------------\------------\---+ | | |
| ---------\ | | WK | |\ | | +-- -|-|-----+ |
| \ | | | start | | \ \ | | | |/| |
| \ | | | | --------\ \ \| | |/| | |
|--------\--------+--------+--------+---|----+----\-\--\|---/|-+-|------|
| | \ | | | | | \ \ |\/ | | | |
| | | | | | | | \ +---+ |
| | | | | | \ | | \ | |
| | | | | | \ | | / | |
|--------+---|----+--------+--------+--------\--------+/-------+--------|
| | | | | | | \ /| | |
| | | | | | | \ / | | |
| | \ | | | | / \ | | |
| | \ | | | | | \| | |
|--------+-------\+--------+--------+--------+---|----+\-------+--------|
| | |\ WK end| | | | | \ | |
| | | \ \ | | | | | \ | |
| | | \ \ | | | | | \------ |
| | | \ \ | | | | | / |
|--------+--------+--------\-\------+--------+---|----+--------+/-------|
| | | | \ \ | | | | /| |
| | | | \ \-----\ | | | / | |
| | | | \ | \ | / | / | |
| | | | \| \ | / | / | |
|--------+--------+--------+--------+\-------/--------/--------+--------|
| | | | | \ / | \ / | | |
| | | | | / | \/ | | |
| | | | | | | | |
| | | | | | | | |
+-----------------------------------------------------------------------+

APPOLONIUS' CIRCLE THEOREM: The altitude pedal of the hypotenuse of
a right-angled triangle and the midpoints of the three sides of the
triangle lie on a circle; i.e. in the figure below, the pedal point
H lies on the circle determined by the midpoints EFG.

B (0,b) #
# #
# #
# # H (h,j)
# *
# * # # *
# * # #
# # # F (f,i)
G (0,g) * # *
# # #
* # # #
# # #
* # # * M (c,d) * #
# # #
* # # #
# # * #
* # #
########################*##########################
C (0,0) * E (e,0) A (a,0)
* *
*

(Hypotheses)
h1 := 2 e - a = 0 (E is midpoint of CA)
h2 := 2 f - a = 0 (F is midpoint of AB, 1st coordinate)
h3 := 2 i - b = 0 (F is midpoint of AB, 2nd coordinate)
h4 := 2 g - b = 0 (G is midpoint of BC)
h5 := (c - e)^2 + d^2 - (c - f)^2 - (d - i)^2 = 0 (length EM = length FM)
h6 := (c - e)^2 + d^2 - c^2 - (d - g)^2 = 0 (length EM = length GM)
h7 := (h - a) b + a j = 0 (H lies on AB)
h8 := - a h + b j = 0 (CH is perpendicular to AB)

(Conclusion)
Z := (c - e)^2 + d^2 - (c - h)^2 - (d - j)^2 = 0 (length EM = length HM)

Appolonius' Circle Theorem is equivalent to the proposition

P(a,b,c,d,e,f,g,h,i,j) :=
for all real numbers a,b,c,d,e,f,g,h,i,j:
if h1, h2, h3, h4, h5, h6, h7, and h8 = 0
then Z = 0


References

[BL] Burris, S., Lawrence, J. Term rewrite rules for finite fields.
Int. J. of Algebra and Computation, vol. 1, No. 3 (1991) 353-369.

[CCC] Computers, Chess, and Cognition, T. Anthony Marsland and
Jonathan Schaeffer (ed.), Springer Verlag 1990.

[CL] Computational Logic: Essays in Honor of Alan Robinson,
J. Lassez and G. Plotkin (ed.), MIT Press, 1991.

[Fe1] Feferman, S. Transfinite recursive progressions
of axiomatic theories. Journal of Symbolic Logic, 27 (1962) 383-390.

[Fe2] Feferman, S. Turing in the land of O(z). In (R. Herken, ed.),
The Universal Turing Machine: A Half-century Survey, pp. 113-147.
Oxford University Press, 1988.

[Fe3] Feferman, S. Penrose's Goedelian Argument: A Review of _Shadows
of the Mind_ by Roger Penrose. PSYCHE: an interdisciplinary journal of
research on consciousness 2(7), May 1995. (Symposium on Roger Penrose's
_Shadows of the Mind_).
http://psyche.cs.monash.edu.au/volume2-1/psyche-95-2-07-shadows-5-feferman.html
ftp://ftp.cs.monash.edu.au/psyche/v2-1/psyche-95-2-07-shadows-5-feferman.txt

[Her] Herschberg, I.S. et. al., Verifying and Codifying
Strategies in a Chess Endgame, [CCC], 183-196.

[Kap] Geometric Reasoning, Deepak Kapur (ed.), MIT Press, 1988.

[KZ] Kapur, D. and Zhang, H., A Case Study of the Completion
Procedure: Proving Ring Commutativity Problems, [CL], 360-394.
See also [BL], and references therein.

[KF] Komissarchik, E.A. and A.L. Futer, Computer Analysis of a
Queen Endgame, Journal of the International Computer Chess
Assoc., vol. 9 (1986) no. 4, 189-198.

[Kop] Kopec, D., Advances in Man-Machine Play, [CCC], 9-32.

[Mic] Michie, D., Brute Force in Chess and Science, [CCC], 239-258.

[Nie] All the Needles in a Haystack: Can Exhaustive Search Overcome
Combinatorial Chaos?
http://nobi.ethz.ch/febi/ex_search_paper/paper.html

[Roy] Roycroft, A.J., Queen and Pawn on b7 against Queen, in booklet
no. 7 of "Roycroft's 5-Man Chess Endgame Series", Chess Endgame
Consultants and Publishers, London, England.

0 new messages