Is the equational theory of generalized boolean algebras decidable? One can easily check by using truth tables whether a propositional formula is a logical identity. Thus, the theory of Boolean algebras is decidable. But a generalized Boolean algebra (GBA), i.e. a Boolean algebra with an optional top element usually called “unit” and sometimes denoted as “$1$”, is necessarily infinite, and such a decision procedure could be more complex. However, such algebras appear to be simple enough for one to expect that their theory is decidable. The universe of set theory with the operations of union, intersection and difference is an example of a "large" GBA -- a GBA over a class.
A GBA is strictly defined as a distributive relatively complemented lattice with $0$ (https://planetmath.org/generalizedbooleanalgebra), or as a lattice with $0$, each principal ideal of which is a Boolean algebra. 
 A: The equational theory of GBAs is exactly the same as the equational theory of Boolean algebras restricted to the language of GBAs (i.e., with only relative complements instead of complements and no $1$).
Indeed, any GBA embeds in a Boolean algebra (by formally adjoining complements).  In detail, if $A$ is a GBA, let $B=\{0,1\}\times A$.  Order $B$ by saying $(0,a)\leq (0,b)$ iff $a\leq b$, $(1,a)\leq(1,b)$ iff $b\leq a$, and $(0,a)\leq(1,b)$ iff $a\wedge b=0$ (and $(1,a)\not\leq(0,b)$ for all $a,b$).  Then it is easy to check that $B$ is a Boolean algebra, and $A$ embeds as a sub-GBA of $B$ via $a\mapsto (0,a)$.  The idea is that $(0,a)$ represents $a$ and $(1,a)$ represents the complement of $a$.
(From the perspective of Boolean rings, a GBA is just a possibly non-unital Boolean ring, and this construction just gives its unitization as an $\mathbb{F}_2$-algebra.  The additive group of the unitization is $\mathbb{F}_2\oplus A$, and multiplication is defined by $(i+a)(j+b)=ij+(ib+ja+ab)$ for $i,j\in\mathbb{F}_2$ and $a,b\in A$.)
So, every equation in the language of GBAs that holds in every Boolean algebra also holds in every GBA (and obviously conversely since every Boolean algebra is a GBA), and so the equational theory of GBAs is decidable (by the same algorithm).
