Automated discovery of single axioms for ortholattices |
| |
| Authors: | W. McCune R. Padmanabhan M. A. Rose R. Veroff |
| |
| Affiliation: | (1) Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL 60439, USA;(2) Department of Mathematics, University of Manitoba, Winnipeg, R3T 2N2, Canada;(3) Department of Mathematics, University of Wisconsin-Madison, Madison, WI 53706, USA;(4) Department of Computer Science, University of New Mexico, Albuquerque, New Mexico 87131, USA |
| |
| Abstract: | We present short single axioms for ortholattices, orthomodular lattices, and modular ortholattices, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. We also give multiequation bases in terms of the Sheffer stroke and in terms of join, meet, and complementation. Proofs are omitted but are available in an associated technical report and on the Web. We used computers extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.Received February 26, 2004; accepted in final form September 14, 2004. |
| |
| Keywords: | 03G10 06B99 |
| 本文献已被 SpringerLink 等数据库收录！ |
|
