Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Date: 10 Sep 93 11:53 -0700
From: Eric Borm <borm@cs.ubc.ca>
To: info-hol <info-hol@cs.uidaho.edu>
Message-Id: <1594*borm@cs.ubc.ca>
Subject: A short history of the "challenge" theorem

  I'd like to thank everyone who responded to the "challenge" of
proving my little theorem.  I found all of the responses very
interesting, and was excited to see that there are theorem provers
available that can prove it automatically.  Here's a brief history of
the theorem.

  About six months ago, I was toying around with an idea for automatic
proof generation based on a semantic tableau.  My first attempt at
this was to try to "codify" my own approach to doing these proofs.  In
examining the structures that the algorithm would have created, I began
to suspect that there were some theorems that it wouldn't be able to
prove.

  When I realized that the naive algorithm wasn't as good as I thought
it was, I set about creating a simple example to demonstrate the
problem.  I did this by applying the algorithm "backwards".  That is,
I created an internal representation for which I could see the proof
but the algorithm couldn't.  Then, I backed this out to a theorem that
would have created that structure.  The result is the theorem you saw
in the "challenge".  

  The typical response to asking someone to prove the theorem is
something like the following:

  "Ok, that looks pretty easy."

  (2-3 minutes later)

  "Hmmm, let me make sure I copied it down correctly..."

  (5-10 minutes later)

  "Are you sure this is a theorem??"

This response and the apparent simplicity of the theorem caught my
attention.  So, the "challenge" wasn't intended to be particularly
difficult, just more difficult that it appeared at first glance.

  Thanks again for all the responses...Eric