Automated reasoning and exhaustive search: Quasigroup existence problems

This is a report of research carried out during 1992 and 1993 in which three different automated reasoning programs—DDPP, FINDER, and MGTP—were applied to a series of exhaustive search problems in the theory of quasigroups. All three of the programs succeeded in solving previously open problems concerning the existence of quasigroups satisfying certain additional conditions. Using different programs has allowed us to cross-check the results, helping reliability. We find this research interesting from several points of view: first, it brings techniques from the field of automated reasoning to bear on a rather different problem domain from that which motivated their development; second, investigating such hard problems leads us to push the limits of what our systems have achieved; and finally, it involves us in serious philosophical issues concerning essentially computational proofs.