Weaker forms of associativity in orthomodular lattices

Computations in orthomodular lattices are rather difficult because there is no known analogue of the standard disjunctive or conjunctive forms from boolean algebras. Tools admitting simplifications of formulas are rather limited. In previous work, we investigated the possibility of finding associative operations in orthomodular lattices that would admit new techniques of theorem proving. It was found that there are only 6 operations in orthomodular lattices which are (already known to be) associative. In this paper, we replaced associativity by more general properties, in particular by the identities that hold in alternative algebras. We have found that there are 8 nonassociative operations in orthomodular lattices satisfying the identities of alternative algebras. For these operations, we clarified the validity of other similar identities, including the Moufang identities. We hope that this effort can contribute to clarifying to what extent the validity of identities in orthomodular lattices can be algorithmized.