Automated Deduction and its Application to Mathematics

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.

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