AbstractThis 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. Copyright 1990 by ACM, Inc.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems -- computation on discrete structures, pattern matching; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic -- mechanical theorem proving; I.1.3 [Algebraic Manipulation]: Languages and Systems -- simplification of expressions; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving -- resolution
General Terms: Algorithms, Theory, Verification
Additional Key Words and Phrases: Boolean algebras, Boolean rings, equational reasoning, Post algebras, primal algebras, unification
Selected papers that cite this one
- Silvio Ghilardi. Unification through projectivity. Journal of Logic and Computation, 7(6):733-752, December 1997.