Computer proof of monotonicity of operations on orthomodular lattices

In this paper we study the monotonicity of binary operations in orthomodular lattices and their distributivity with respect to the lattice operations. We present several steps to reduce the amount of computations which would be necessary otherwise, if even possible. The methods, in combination, allow to characterize all monotonic orthomodular lattice operations. Consequences for the (non-)existence of normal forms of expressions in orthomodular lattices are discussed.