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

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

Dates: June 24 -- 26, 2011 (Friday -- Sunday)
Location: Banff International Research Station for Mathematical Innovation and Discovery (BIRS), Banff, Alberta, Canada
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.

### Talks

• Churchhill - Normal Forms in Graded Lie Algebras
• Ens and Padmanabhan - Group Embeddings of Configurations with Prover9 (abstract)
• Ernst - A Syntactic Approach to Automated Deduction
• Padmanabhan and Zhang - Commutativity Theorems in CL-Semirings (abstract)
• Phillips - Bol-Moufang Groupoids of "Group-like" Type
• Sutcliffe - The TPTP Typed First-order Form with Arithmetic (talk)
• Veroff - Working Our Way Up a Theory Hierarchy (talk, AIM problem description)
• Vojtechovsky - Model Builders, Automated Deduction and Automorphic Loops

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