ADAM 2011

Automated Deduction and its Application to Mathematics

It is with great sadness that we announce the untimely passing of our friend and colleague Bill McCune. Bill's contributions have had profound impact; he will be sorely missed. ADAM 2011 will be dedicated to Bill's memory. Here is a brief bio.

ADAM Home Page

The ADAM workshop covers applications of automated deduction to problems in abstract logic and algebra, focusing primarily on algebra and equational problems.

The workshops typically consist of several informal and semi-formal presentations with a great deal of discussion. To help foster a productive working atmosphere, the workshop is limited each year to 10 to 15 people. Participation is by invitation only.

Questions? Contact R Padmanabhan, Yang Zhang or Bob Veroff.

Local Arrangements

See the BIRS Web site.



Additional information about the presentations appears in the workshop report.

Contributed Problems and Other Material

Here is an example to illustrate the use of Autosketches as an implementation of the proof sketches method. The theorem proved is that in a ring, x^5 = x implies commutativity.

Autosketches was started with the following extra assumptions.

   10x = 0.
   5xy + 5yx = 0.
   4xy + 6yx = 0.
   3xy + 7yx = 0.
   2xy + 8yx = 0.
   1xy + 9yx = 0.
Here are the relevant input, output, proof and xml files: (
in, out, pf, xml)

The multiple proofs correspond to the Autosketches iterations. The final proof relies on no extra assumptions.

Note that the extra assumptions happen to be proper extensions of the target theory (ring + x^5 = x) rather than being hints about lemmas to prove in the target theory.

Return to ADAM Home Page

Last Modified: August 3, 2011 by