#### Unification in Primal Algebras, Their Powers and Their Varieties

#### Tobias Nipkow

This paper examines the unification problem in the class of primal algebras
and the varieties they generate. An algebra is called primal if every
function on its carrier can be expressed just in terms of the basic
operations of the algebra. The two-element Boolean algebra is the simplest
non-trivial example: every truth-function can be realized in terms of the
basic connectives, for example negation and conjunction.
It is shown that unification in primal algebras is unitary, i.e. if an
equation has a solution, it has a single most general one. Two unification
algorithms, based on equation solving techniques for Boolean algebras due to
Boole and Löwenheim, are studied in detail. Applications include certain
finite Post algebras and matrix rings over finite fields. The former are
algebraic models for many-valued logics, the latter cover in particular
modular arithmetic.

Then unification is extended from primal algebras to their direct powers
which leads to unitary unification algorithms covering finite Post algebras,
finite, semisimple Artinian rings, and finite, semisimple non-abelian groups.

Finally we use the fact that the variety generated by a primal algebra
coincides with the class of its subdirect powers. This yields unitary
unification algorithms for the equational theories of Post algebras and
p-rings.

BibTeX:

@article{Nipkow-JACM,
author="Tobias Nipkow",
title="Unification in Primal Algebras, Their Powers and Their Varieties",
journal=JACM,year=1990,volume=37,pages="742--776"}