Publications

M. Rose and K. Wilkinson, "Application of Model Search to Lattice Theory," Preprint ANL/MCS-P900-0801, August 2001.

We have used the first-order model-searching programs MACE and SEM to study various problems in lattice theory. First, we present a case study in which the two programs are used to examine the differences between the stages along the way from lattice theory to Boolean algebra. Second, we answer several questions posed by Norman Megill and Mladen Pavicic on ortholattices and orthomodular
lattices. The questions from Megill and Pavicic arose in their study of quantum logics, which are being investigated in connection with proposed computing devices based on quantum mechanics. Previous questions of a similar nature were answered by McCune and MACE in W. McCune, "Automatic Proofs and Counterexamples for Some Ortholattice Identities," Information Processing Letters 65 (1998), pp. 285-291.

MACE (Models And Counter Examples) (W. McCune, "MACE 2.0 Reference Manual and Guide," Tech Memo ANL/MCS-TM-249, MCS Division, Argonne National Laboratory, Argonne, IL, June 2001) and SEM (System for
Enumerating Models) (J. Zhang and H. Zhang, "SEM: A System for Enumerating Models. In Proceedings of the International Joint Conf. on AI, Morgan Kaufmann, 1995) are programs that search for finite models of first-order and equational logic statements. If the input statement is the denial of a conjecture, then any models found are counterexamples. MACE searches for models by transforming its input into an equiconsistent propositional problem, then calling a
Davis-Putnam-Loveland-Logeman procedure. SEM uses a more direct method of filling in tables according to various heuristics and evaluating the input against the tables. SEM is usually more effective than MACE for problems with large formulas. Both programs are designed to be complete; that is, if the search for a model of size n terminates without finding a model, then there should be none of that size. We believe the lattices we present in this note are the smallest ones satisfying the given properties, because the programs reported that smaller examples do not exist.

This note has a companion page on the World Wide Web. The page
http://www.mcs.anl.gov/AR/aar_lattice contains links to MACE, SEM, and EQP input files and other data files related to this work. In this note, we refer to those files with bold-faced underlined pseudolinks like this.