Unification in Boolean rings (Q1112626)

The prime concern of this paper is a concise exposition of unification in Boolean rings using Löwenheim's method. Following a brief but instructive introduction of Boolean rings Löwenheim's theorem on unification of Boolean terms by their most general unifier is proven. Arbitrary Boolean rings can easily be transformed to represent each of its elements in terms of an orthogonal basis. This orthogonal normal form of Boolean terms constitutes the starting point of the unification algorithm that is presented here designed to lower time complexity considerably. Eventually the impact of this algorithm applied to solve unification problems in set theory as well as in propositional calculus is demonstrated by examples.