Tue, 18 Apr 2023, 11 am MDT
In this talk I will report on some joint research in the past year with J.B. Nation and Ralph Freese on ortholattices and with Melissa Sugimoto, José Gil-Férez and Sid Lodhia on involutive partially ordered monoids. Rather than just present the results I will attempt to describe how the automated theorem prover Prover9/Mace4 was used in some aspects of this research. For ortholattices we prove that the variety $\mathcal H$ generated by the 6-element hexagonal ortholattice has an equational basis given by any equational basis of the pentagon lattice variety. We find a list of 9 finite ortholattices that generate varieties covering $\mathcal H$ and present partial results towards showing that this list of finitely generated covers is exhaustive. For locally integral involutive po-monoids we prove that they are Plonka sums of integral involutive po-monoids and we give a more compact dual description of these sums. These results generalize an earlier structural description of finite commutative idempotent involutive residuated lattices by replacing the lattice order by a partial order, idempotence by local integrality and removing finiteness and commutativity. In the idempotent lattice-ordered case we give equational bases for finitely generated varieties by relating them to varieties of Brouwerian algebras.