Slaney's Quasigroups

• A cancellative monoid, i.e.,
• The operator forms a Latin Square, i.e.,
• Each row and column is a permutation of the elements
• Related to design theory
• Many hard combinatorial problems
• I'm just a logician who trusts mathematicians

Using ATP

• Finite model finders: DDPP, FINDER, MGTP
• Questions asked and answered, e.g.,
  Is there a Schröder quasigroup order 12 - Yes!
• Questions asked and unanswered, e.g.,
  Is there a (3,2,1)-COILS(12)? - Too hard :-(

Is it Mathematics?

• Back then, a divided mathematical community
• Now, well accepted
• Famous results
  • Appel and Haken's four colour theorem
  • Hales' proof of the Keppler conjecture
  • Heule's Schur number 5 (=161)