The XCB problem has been solved!
On April 13, 2002, at 4:37 p.m.,
my colleagues and I solved -- in the affirmative -- the XCB open problem
in equivalential calculus.
I am working in the area of automated reasoning,
developing new strategies and inference rules that can be implemented in automated
reasoning programs. We have made significant gains in automated reasoning in the
past few years, as the figure below shows.
For examples of significant challenges (on a Ph.D. level) remaining in the area of
automated reasoning, see, for example, "The Problem of Reasoning
by Analogy" and "The Problem of Reasoning
by Case Analysis."
One of my recent interests is seeking (and finding!) shorter proofs for challenging
problems. I encourage researchers to take the files and seek even shorter proofs. Some of
the problems are in Boolean algebra, others in quasi-lattices, and still others in equivalential calculus. See also An Experimenter's Notebook.
In response to a frequent request, I have put on the Web a few puzzles that interested
students and more advanced researchers may find challenging. The puzzles include the jobs puzzle, the missionaries and cannibals puzzle, the dominoes checkerboard puzzle, the truthtellers puzzle, and the puzzle of fifteen.
Much of the recent success that the Argonne group has enjoyed in automated reasoning is
attributable to the powerful reasoning program Otter,
developed by W. McCune. Otter has been used to answer numerous challenging questions in
mathematics and logic.
Papers, Reports and Talks
Mathematics and Computer Science Division
Argonne National Laboratory
9700 S Cass Ave
Argonne, IL 60439