Larry Wos

What's New

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."

Current Projects

Shorter Proofs

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.

Puzzles

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.

Otter

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

Addresses

Mathematics and Computer Science Division
Argonne National Laboratory
9700 S Cass Ave
Argonne, IL 60439

FAX: 630-252-5986

wos@mcs.anl.gov