[FOM] advances in busy beaver problem & auto thm proving

[vznuri@earthlink.net]

hi all, its been awhile since I last posted. just wanted to
tip you off on some neat new research with potentially deep
implications.

the busy beaver problem which asks, "how many turing machines of
size n states halt?" is undecidable in general, but some enterprising
algorithmists have devised ingenious algorithms that have in fact
resolved the problem for small n, with increasing improvements
in the "technology". 

and with a little imagination it has significant
implications for theorem proving research & automated theorem proving
applications. (to the degree that most, perhaps even _all_
of math thm proving, can
be rephrased in terms of questions about halting of tm's).

one of the nicer recent research drives is by a group ata
renssellaer entitled "a new millenium attack on the busy beaver problem"

http://www.cs.rpi.edu/~kelleo/busybeaver/

this is a sophisticated masters thesis by owen kellet, one of the 
leading inquirers

http://www.cs.rpi.edu/~kelleo/busybeaver/downloads/OwenThesis.pdf


Im delighted to be able to mention that owen kellet has 
just posted an email to the mailing list I moderate, theory-edge.
you can find our musings here. maybe you'd like to drop by & participate
in the discussion.

http://groups.yahoo.com/group/theory-edge/

* * *

I would also like to invite anyone from this elite group of researchers
assembled on FOM to join us & myself in busy-beaver type inquiry.

I have been devising some algorithms in related areas for over a
decade & would be interested in corresponding with anyone, esp
those with a desire/capability for original research. I also think
this has a deep connection to "reversible mathematics" which has
been championed by some on this list.

just to summarize, one of my ideas was as follows: using ruby, I actually
built a tm that runs the following program:

a. enumerate all (a,b) integer pairs in "canonical" order. (b<a)
b. compute a+b, and also b+a
c. halt if a+b != b+a

based on the simple commutivity of integer addition,
this program never halts.

now, the trick is to prove it!! preferrably, using an algorithm that
can analyze the above TM. this is quite nontrivial and, surprisingly,
apparently beyond the capabilities of all modern automated thm proving
systems (afaik).

yet, I think I can devise an algorithm that could do it. its in development.

for further details, drop me an email.