Automated Deduction and its Application to Mathematics

The ADAM workshop covers applications of automated deduction to problems in abstract logic and algebra, focusing primarily on algebra and equational problems. ADAM 2007 is sponsored by the Computer Science Department of the University of New Mexico, Albuquerque.

Dates: June 21 -- 23, 2007 (Thursday -- Saturday)
Location: University of New Mexico, Albuquerque, New Mexico

Questions? Contact Bob Veroff or Bill McCune.

Local Arrangements

Google map of the area around the Fairfield Inn.

The Computer Science Department office is on the first floor of Farris Engineering Center (FEC). The workshop will be in the CS Department conference room, FEC 141.

Map of the area around FEC.
Campus map. FEC is Building #119, near the lower-left (southwest) corner of this map.

Participants

• Zac Ernst, University of Missouri-Columbia
• Nikolaos Galatos, Japan Advanced Institute of Science and Technology
• Peter Jipsen, Chapman University
• Michael Kinyon, University of Denver
• William McCune, University of New Mexico
• R Padmanabhan, University of Manitoba
• J. D. Phillips, Wabash College
• Kyle Pula, University of Denver
• Matthew Spinks, University of Cagliari
• David Stanovsky, Charles University in Prague, Czech Republic
• Bob Veroff, University of New Mexico
• Petr Vojtechovsky, University of Denver

Talks

• Ernst
  • A Procedure for Automatically Discovering Infinite Countermodels (pdf)
• Jipsen
  • Searching for finite algebraic structures using the computer algebra system SAGE
• Kinyon
  • A Variety Containing Quasi-Hilbert Algebras (pdf)
• McCune
  • Robbins with Definitions
  • LADR/Prover9/Mace4 Update
• Padmanabhan
  • Ternary modular algebras
  • Experiments with Prover9 (and Mace4)
• Phillips
  • Open Questions in Loop Theory
• Pula
  • Using Prover9/Mace4 to Understand Jordan Loops (pdf)
• Spinks
  • On the assertional logic of the generic double-pointed discriminator variety (pdf)
  • On the poset structure of n-potent right ideal commutative BCK-algebras (pdf)
  • On the application of automated reasoning to the solution of higher-order problems
• Stanovsky
  • Using automated reasoning in universal algebra: several examples (talk, problem)
• Petr Vojtechovsky
  • Code Loops and Prover9
• Veroff
  • Proof Sketches Discussion (talk, example)

Contributed Problems and Other Material

• HBCK (Spinks)
• NBCK (Spinks)
• QHA (Spinks)
• Axiomatising Implicational Subreducts of N-potent Residuated Lattices (Spinks)

  This problem originated with C. J. van Alten, who reports that no progress has been made on the problem since it was posted for ADAM 2006. It is known that there are no countermodels with <= 14 elements.

Return to ADAM Home Page