Mathematics and Computer Science DivisionThe focus of the workshop will be on practical applications of automated reasoning to problems in axiomatics of algebras and logics. The workshop will be very informal, with about half of the time given to short (20 minutes or less) talks, with plenty of time for discussion.

Argonne National Laboratory

July 10--12, 2003 (Thursday 9AM -- Saturday noon).

The goal is to have a mix of mathematicians, logicians, and automated deduction experts so that we can exchange problems and automated reasoning techniques.

As for the previous AWARD workshops, we will probably have no budget, except maybe for coffee and cookies.

- Most out-of-towners will be staying at the Argonne Guest House, which is a 10-minute walk to the workshop site (Building 221).
- Judy Beumer (beumer@mcs.anl.gov)
will be arranging gate passes for participants and handling some
of the other paperwork.
*Thanks Judy!* - Here's the e-mail with the details.
- Here's the reminder e-mail.
- Current arrival data.

Send any questions to mccune@mcs.anl.gov or wos@mcs.anl.gov.

- Michael Beeson,
San Jose State University

"I'll be there." - Johan Belinfante,
Georgia Tech

"I intend to attend." - Bob Boyer,
UT at Austin

declined - Stan Burris,
University of Waterloo

declined - Mike Dunn,
Indiana University

declined - Zac Ernst,
Florida State University

"My answer is an enthusiastic 'Yes'." - Branden Fitelson,
UC Berkeley

"I'll be there!" - Kenneth Harris,
University of Chicago

"I am very interested in attending." - Ken Keefe,
Southern Illinois University and Argonne National Laboratory

accepted - Kenneth Kunen,
University of Wisconsin

declined - Olga Matlin,
Argonne National Laboratory

declined - Bill McCune,
Argonne National Laboratory

accepted - Norm Megill,
Metamath

"I accept. Thanks!" - Bob Meyer,
Australian National University

"Looks good! HOPE I can make it! NO promises!" - Ross Overbeek,
Argonne National Laboratory

"I will certainly try to attend." - J. D. Phillips,
Wabash College

"Sounds like fun; count me in!" - R Padmanabhan,
University of Manitoba

accepted - Mike Rose,
University of Wisconsin

declined - John Slaney,
Australian National University

no response - Mark Stickel,
SRI

"Sounds like fun; I intend to attend." - Ted Ulrich,
Purdue University

"Sure, I'll be there." - Bob Veroff,
University of New Mexico

accepted - Larry Wos,
Argonne National Laboratory

accepted

- Fitelson: A Probability Machine with Applications
- Beeson: Second Order Proofs in Otter

- Padmanabhan: Analogs of Levy's Problems for Cancellative Semigroups and Loops
- Phillips: Using Otter to Solve Problems in Loop Theory
- McCune: Argonne Deduction Software Update

- McCune: Sheffer Stroke Bases for Ortholattices
- Megill: Orthomodular Lattices and Beyond
- Belinfante: Associative Relations
- Wos: Avoiding the Formula KEY

- Stickel: Finding Very Short Proofs
- Ulrich: Beyond the 1- and 1-2 Properties: Finding Single Axioms that are D-complete
- Ernst: Fun with YQE

- Bob Meyer: Associativity

- Norm Megill's Workshop Miscellany Page
- Examples of complicated CD inferences from Larry Wos's XCB proofs:
- LR Associativity problems suggested by Bob Meyer
- Previous workshops: