Automated Deduction and its Application to Mathematics

ADAM 2006

Automated Deduction and its Application to Mathematics

This workshop is a successor to the series of workshops held at Argonne the past few summers (AWARD-2001 -- AWARD-2005). The Argonne workshops covered applications of automated deduction to problems in abstract logic and algebra. The ADAM workshop will focus mainly on algebra and equational problems. Like the Argonne workshops, the ADAM workshop will also emphasize automated deduction methods. ADAM 2006 is sponsored by the Computer Science Department of the University of New Mexico, Albuquerque.

Questions? Contact Bob Veroff or Bill McCune.

Local Arrangements

Recommended hotel: Fairfield Inn, Albuquerque University Area (Contact Bob for details.)

Google map

We will be meeting in Farris Engineering Center (FEC), Room 141. Bob's office is FEC 153.

Map

Campus map

Participants

Zac Ernst, University of Missouri-Columbia
Adam Gareau, University of Manitoba
Peter Jipsen, Chapman University
Deepak Kapur, University of New Mexico
Michael Kinyon, University of Denver
William McCune, Argonne National Laboratory
R Padmanabhan, University of Manitoba
J. D. Phillips, Wabash College (unable to attend)
Matthew Spinks, La Trobe University (unable to attend)
Bob Veroff, University of New Mexico
Petr Vojtechovsky, University of Denver

Talks

Ernst
- Infinite Models of Propositional Calculi
Gareau
- Some CS-commutativity Theorems
Jipsen
- The Mathematical Structures pages: current status and future plans (abstract)
Kinyon
- Loop theory problems for which automated deduction might be useful
McCune
- Semantic Guidance in Prover9
- Prover9/Mace4 Updates
Padmanabhan
- Huntington's Conjecture Revisited
Veroff
- Welcome
- Proof Sketches with Prover9 (slides, Autosketches examples)
Vojtechovsky
- Semi-boolean algebras and implication algebras

Contributed Problems and Other Material

Axiomatising Implicational Subreducts of N-potent Residuated Lattices Corrected version (Spinks)
Comment: This problem originated with C. J. van Alten. It is known that there are no countermodels with <= 14 elements.
Here is the version that was originally posted. Michael Kinyon found a 10-element countermodel with Mace4, which led to the discovery of the error in the problem statement.
HBCK (Spinks)
quasi-Hilbert algebras (Spinks)
Implication Algebras (Gareau and Padmanabhan)

The AWARD Workshops at Argonne National Laboratory

Last Modified: October 20, 2006 by veroff@cs.unm.edu