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

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.

### Participants

- Richard Churchill,
City College of New York
- Eric Ens,
University of Manitoba
- Zac Ernst,
University of Missouri-Columbia
- R Padmanabhan,
University of Manitoba
- J. D. Phillips,
Northern Michigan University
- Geoff Sutcliffe,
University of Miami
- Bob Veroff,
University of New Mexico
- Petr Vojtechovsky,
University of Denver
- Qiduan Yang,
University of British Columbia
- Yang Zhang,
University of Manitoba

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

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 veroff@cs.unm.edu