Involutive lattices are distributive lattices with an
involution satisfying De Morgan laws; for instance, Boolean algebras
are complemented involutive lattices. For a fixed algebraic variety,
(equational) unification is the problem of solving equations in the
context of free algebras. The solutions to a particular instance of
the unification problem are ordered by generality in a natural way.
Algorithmically, the instance is nice or bad depending on whether or not
the set of all solutions admits a subset of finitely many pairwise incomparable
most general solutions, and the type of an instance (nullary, unary,
finitary, or infinitary) includes this information. By reducing the classification to the
classification of a suitable class of finite posets, we classify all
instances of the unification problem over involutive lattices with
respect to their types.

An algebra is said to be finitely based if there is a finite subset of its identities from which all of its identities may be deduced. Let $A$ be an alphabet and $W$ be a set of words in a free monoid $A*$. Let $S(W)$ denote the Rees quotient over the ideal of $A*$ consisting of all words that are not subwords of words in $W$. We call a set of words $W$ finitely based if the monoid $S(W)$ is finitely based.

A letter $x$ in a word $u$ is called linear if $x$ occurs once in $u$, otherwise $x$ is called non-linear.

We find a simple algorithm that recognizes finitely based words among the words in at most two non-linear letters.

Reading Group: Rossman, B, “Homorphism Preservation Theorems”, Journal of the ACM, July 2008

Reading Group: Rossman, B, “Homorphism Preservation Theorems”, Journal of the ACM, July 2008

Reading Group: Rossman, B, “Homorphism Preservation Theorems”, Journal of the ACM, July 2008