Challenge Equality Problems in Lattice Theory
This note contains five problems that should be useful for experimentation with equalityoriented automated theorem-proving programs. The problems are formally stated and proved in first-order predicate calculus with equality. The problems are taken from the often-overlooked paper "Semi-automated mathematics" by Guard et al. [Guard69]. That paper focuses on an interactive theorem prover, SAM, which was instrumental in solving an open problem in lattice theory (Theorem L3 below) posed by Bumcroft [Bumcroft65]. That achievement marked an important advance for the field of automated theorem proving.