Unification in primal algebras

  • Tobias Nipkow
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)


Unification in primal algebras is shown to be unitary. Three different unification algorithms are investigated. The simplest one consists of computing all solutions and coding them up in a single vector of terms. The other two methods are generalizations of unification algorithms for Boolean algebras.

Two applications are studied in more detail: Post algebras and matrix rings over finite fields. The former are algebraic models for many-valued logics, the latter cover in particular modular arithmetic.

It is indicated that the results extend to arbitrary varieties of primal algebras which include all Boolean and Post algebras and p-rings.


Boolean Algebra Finite Field Function Symbol Unification Algorithm Matrix Ring 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BaChJo 84]
    H. Barringer, J.H. Cheng, C.B. Jones: A Logic Covering Undefinedness in Program Proofs, Acta Informatica 21, 251–269, 1984Google Scholar
  2. [Bo 1847]
    G. Boole: The Mathematical Analysis of Logic, Macmillan 1847. Reprinted 1948, B. Blackwell.Google Scholar
  3. [BüSi 87]
    W. Büttner, H. Simonis: Embedding Boolean Expressions into Logic Programming, to appear in Journal of Symbolic Computation, 1987Google Scholar
  4. [Ch 86]
    J.H. Cheng: A Logic for Partial Functions, Ph.D. Thesis, Dept. of Comp. Sci., The University of Manchester, 1986Google Scholar
  5. [Co 86]
    H. Comon: Sufficient Completeness, Term Rewriting Systems and Anti-Unification, in: 8th Int. Conf. on Automated Deduction, LNCS 230, 1986Google Scholar
  6. [Fo 53]
    A.L. Foster: Generalized “Boolean” Theory of Universal Algebra, Math. Zeitschr. 59, 1953, 191–199Google Scholar
  7. [FoPi 64]
    A.L. Foster, A. Pixley: Semi-Categorical Algebras. I. Semi-Primal Algebras, Math. Zeitschr. 83, 1964, 147–169Google Scholar
  8. [GaJo 79]
    M.R. Garey, D.S. Johnson, Computers and Intractability, W.H. Freeman and Company, San Francisco, 1979Google Scholar
  9. [Gr 79]
    G. Grätzer: Universal Algebra, Second Edition, Springer Verlag, 1979Google Scholar
  10. [He 68]
    I.N. Herstein: Noncommutative Rings, The Mathematical Association of America, 1968Google Scholar
  11. [Kn 70]
    R.A. Knoebel: Simplicity vis-à-vis Functional Completeness, Math. Ann. 189 (1970), 299–307Google Scholar
  12. [Lö 08]
    L. Löwenheim: Über das Auflösungsproblem im logischen Klassenkalkül, Sitzungsber. Berl. Math. Gesell. 7, 89–94, 1908Google Scholar
  13. [MaNi 86]
    U. Martin, T. Nipkow: Unification in Boolean Rings, in: 8th Int. Conf. on Automated Deduction, LNCS 230, 1986, 506–513Google Scholar
  14. [MaNi 88]
    U. Martin, T. Nipkow: Boolean Unification — A Survey, to appear in Journal of Symbolic ComputationGoogle Scholar
  15. [Ni 87]
    T. Nipkow: Unification in Primal Algebras, their Powers and their Varieties, in preparationGoogle Scholar
  16. [Po 21]
    E.L. Post: Introduction to a General Theory of Elementary Propositions, Amer. J. Math. 43, 163–185, 1921Google Scholar
  17. [Ra 74]
    H. Rasiowa: An Algebraic Approach to Non-Classical Logics, North-Holland, 1974Google Scholar
  18. [Ru 74]
    S. Rudeanu: Boolean Functions and Equations, North-Holland, 1974Google Scholar
  19. [Sch 90]
    E. Schröder: Vorlesungen über die Algebra der Logik, (Leipzig, Vol 1, 1890; Vol 2, 1891, 1905; Vol 3, 1895), Reprint 1966, (Chelsea, Bronx NY)Google Scholar
  20. [St 36]
    M.H. Stone: The Theory of Representation for Boolean Algebras, Trans. Amer. Math. Soc. 40, 1936, 37–111Google Scholar
  21. [Ti 86]
    E. Tidén: Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols, in 8th International Conference on Automated Deduction, Lecture Notes in Computer Science 230, Springer 1986, 431–449Google Scholar
  22. [We 78]
    H. Werner: Einführung in die allgemeine Algebra, Bibliographisches Institut, Mannheim, Wien, Zürich, 1978Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Tobias Nipkow
    • 1
  1. 1.Department of Computer ScienceUniversity of ManchesterManchester

Personalised recommendations