# Is there an (efficient) algorithm to determine whether an equation of two terms in the language of elementary set theoretic operators is an identity?

By elementary set theoretic operations I refer to those which are usually imaged in Venn diagrams -- union, intersection, set difference, etc. In the formulation of my question I included the word efficient'' between parentheses because in computing complexity this term is used with different meanings and here I am not very interested in complexity. I would like to learn about any algorithm which would not just "exhaust all possibilities" (like substituting 0s and 1s, in case of boolean terms), an algorithm which would be useful or instructive when implemented as a computer program.

This question naturally came after another question of mine: Is the equational theory of generalized boolean algebras decidable?

The theory you describe is decidable, by the algorithm you mentioned but don't want, namely substituting 0's and 1's in all possible ways. Indeed, deciding whether a Boolean equation (using $$\cap,\cup,-$$) is an identity amounts to deciding whether a formula in propositional logic is a tautology. Whether this can be done in polynomial time is a big open problem (the P=NP problem). Nevertheless, much is known about algorithms that, in many cases, work much better than the plug-in-0's-and-1's algorithm. In particular, people have programmed heuristics for guessing which combinations of 0's and 1's are likely to give counterexamples. I'm not an expert on these methods, but until an expert comes along and gives you a better answer, you could google "SAT-solvers" and find a good deal of information. ("SAT" refers to the problem of deciding whether a formula in propositional logic is satisfiable; that's equivalent to asking whether the formula's negation is not a tautology, so it's essentially the same question for your purposes.)