Unification in primal algebras, their powers and their varieties

ABSTRACT

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 nontrivial 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, that is, 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 Lo¨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 nonabelian groups. Finally the fact that the variety generated by a primal algebra coincides with the class of its subdirect powers is used. This yields unitary unification algorithms for the equational theories of Post algebras and p-rings.

REFERENCES

• 1: BARRINGER, H., CHENG, J. H., AND JONES, C. B. A logic coveting undefinedness in program proofs. Acta Inf. 21 (1984), 251-269.
• 2: BOOLE, G. The Mathematical Analysis of Logic. Macmillan, New York, 1847. Reprinted: B. Blackwell, London, England, 1948.
• 3: Wolfram Büttner , Helmut Simonis, Embedding Boolean expressions into logic programming, Journal of Symbolic Computation, v.4 n.2, p.191-205, Oct. 1987 [doi>10.1016/S0747-7171(87)80065-2]
• 4: CHENG, J.H. A logic for partial functions. Ph.D. Thesis. Dept. ofComput. Sci., Univ. Manchester, Manchester, England, 1986.
• 5: COLMERAUER, A. Prolog II Reference Manual and Theoretical Model. Groupe Intelligence Artificielle, Facult6 des Sciences de Luming, Marseilles, France, 1982.
• 6: H Comon, Sufficient completeness, term rewriting systems and “anti-unification”, Proc. of the 8th international conference on Automated deduction, p.128-140, August 1986, Oxford, United Kingdom
• 7: FOSTER, A. L. Generalized "Boolean" theory of universal algebra. Math. Zeitschr. 59 (1953), 191-199.
• 8: FOSTER, A. L., AND PIXLEY, A. Semi-categorical algebras. I. Semi-primal algebras. Math. Zeitschr. 83 (1964), 147-169.
• 9: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 10: S. J. Garland , J. V. Guttag, An overview of LP, the larch power, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.137-151, January 1989
• 11: GRATZER, G. UniversalAlgebra, 2nd Ed. Springer-Verlag, New York, 1979.
• 12: HERSTEIN, I.N. Noncommutative Rings. The Mathematical Association of America, Washington, DC, 1968.
• 13: Jieh Hsiang, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, v.25 n.3, p.255-300, March 1985 [doi>10.1016/0004-3702(85)90074-8]
• 14: Deepak Kapur , Paliath Narendran, Matching, unification and complexity, ACM SIGSAM Bulletin, v.21 n.4, p.6-9, Nov. 1987 [doi>10.1145/36330.36332]
• 15: KNOEBEL, R.A. Simplicity vis-fi-vis functional completeness. Math. Ann. 189 (1970), 299-307.
• 16: LOWENHEIM, L. Uber daN Aufl6sungsproblem im logischen Klassenkalkiil. Sitzungsber. Berl. Math. Gesell. 7 (1908), 89-94.
• 17: U Martin , T Nipkow, Unification in Boolean rings, Proc. of the 8th international conference on Automated deduction, p.506-513, August 1986, Oxford, United Kingdom
• 18: Ursul Martin , Tobias Nipkow, Unification in Boolean rings, Journal of Automated Reasoning, v.4 n.4, p.381-396, Dec. 1988 [doi>10.1007/BF00297246]
• 19: Ursula Martin , Tobias Nipkow, Boolean unification—the story so far, Journal of Symbolic Computation, v.7 n.3-4, p.275-293, March/April 1989 [doi>10.1016/S0747-7171(89)80013-6]
• 20: MARTIN, U., AND NIPKOW, T. Canonical Term Rewriting Systems for p-Rings. Tech Rep. In preparation.
• 21: McCoY, N. H., AND MONTGOMERY, D. A representation of generalized Boolean tings. Duke Math. J. 3 (1937), 455-459.
• 22: POST, E.L. Introduction to a general theory of elementary propositions. Amer. J. Math. 43 ( 1921), 163-185.
• 23: RASIOWA, H. An Algebraic Approach to Non-Classical Logics. North-Holland, Amsterdam, The Netherlands, 1974.
• 24: RATH, H.H. Ein Meta-Interpretierer f'tir Prolog mit Boolescher Unifikation. KAP-MEMO 1/88, SFB 314, Universit/it Karlsruhe, Karlsruhe, West Germany, 1988.
• 25: ROSENBLOOM, P.C. Post algebras. I. Postulates and general theory. Amer. J. Math. 64 (1942), 167-188.
• 26: RUDEANU, S. Boolean Functions and Equations. North-Holland, Amsterdam, The Netherlands, 1974.
• 27: Manfred Schmidt-Schauß, Unification in a Combination of Arbitrary Disjoint Equational Theories, Proceedings of the 9th International Conference on Automated Deduction, p.378-396, May 23-26, 1988
• 28: SCHRODER, E. Vorlesungen fiber die Algebra der Logik. Leipzig, Vol 1, 1890; Vol 2, 1891, 1905; Vol 3, 1895; Reprint 1966, Chelsea, Bronx, New York.
• 29: Jörg H. Siekmann, Unification theory, Journal of Symbolic Computation, v.7 n.3-4, p.207-274, March/April 1989 [doi>10.1016/S0747-7171(89)80012-4]
• 30: STONE, M. H. The theory of representation for Boolean algebras. Trans. Amer. Math. Soc. 40 (1936), 37-111.
• 31: E Tidén, Unification in combinations of collapse-free theories with disjoint sets of function symbols, Proc. of the 8th international conference on Automated deduction, p.431-449, August 1986, Oxford, United Kingdom
• 32: WERNER, H. EinJ~hrung in die allgemeine Algebra. Bibliographisches Institut Mannheim/Wien/ Ziirich, 1978.
• 33: Kathernie A. Yelick, Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, v.3 n.1-2, p.153-181, Feb./April 1987 [doi>10.1016/S0747-7171(87)80025-1]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Simplification of expressions
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

General Terms:
Algorithms, Theory