# 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

On-line versions of recent papers

An Interesting Bio by T. Obermiller

## Addresses

Mathematics and Computer Science Division

Argonne National Laboratory

9700 S Cass Ave

Argonne, IL 60439

FAX: 630-252-5986

wos@mcs.anl.gov