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.
orthomodular lattice free lattice generator orthocomplement kalmbach embedding horizontal sum