Embedding boolean expressions into logic programming

Boolean expressions play a major role in computer science. They can be used to represent sets, formulas of propositional logic and digital circuits. In this paper we present an algorithm to compute the most general unifier (mgu) of boolean expressions, which is unique, if it exists. The fact that there is always at most one mgu, i.e. the theory of boolean expressions is unitary, is of particular importance for the embedding of the data type ‘boolean expression’ into logic programming. First experiemes with an integration into a PROLOG system are shown.